Require Import ChargeCore.Logics.ILogic.
Require Import Setoid Morphisms RelationClasses Program.Basics Omega.

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Section ILogicEmbed.
  Context {A} `{ILOpsA: ILogicOps A}.
  Context {B} `{ILOpsB: ILogicOps B}.

  Class EmbedOp : Type := { embed : A -> B }.

(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
  Class Embed {EmbOp: EmbedOp} : Type := {
     embed_sound p q : p |-- q -> embed p |-- embed q;

     embedlforall T f : Forall x : T, embed (f x) -|- embed (Forall x : T, f x);
     embedlexists T f : Exists x : T, embed (f x) -|- embed (Exists x : T, f x);
     embedImpl a b : (embed a) -->> (embed b) -|- embed (a -->> b)
  }.
End ILogicEmbed.

Arguments EmbedOp _ _ : clear implicits.
Arguments Embed _ {ILOpsA} _ {ILOpsB EmbOp} : rename.

Section ILogicEmbedOps.
  Context {A B} `{HAB: Embed A B} {ILA: ILogic A} {ILB: ILogic B}.

  Definition lembedand (a : A) (b : B) := (embed a) //\\ b.
  Definition lembedimpl (a : A) (b : B) := (embed a) -->> b.

End ILogicEmbedOps.


Section ILEmbedId.

  Context {A : Type} `{ILA : ILogic A}.

  Instance EmbedOpId : EmbedOp A A := { embed := id }.
  Global Instance EmbedId : Embed A A.
  Proof.
(* Goal: @Embed Prop ILogicOps_Prop Prop ILogicOps_Prop EmbedOpPropProp *)
    split; firstorder.
  Qed.

End ILEmbedId.

Section ILogicEmbedCompose.
  Context {A B} `{HAB: Embed A B} {ILA: ILogic A} {ILB: ILogic B}.
  Context {C} {HC: ILogicOps C} {HE: EmbedOp B C} {HBC : Embed B C} {ILC: ILogic C}.

  Instance embedOpCompose : EmbedOp A C := { embed := fun x => embed (embed x) }.

  Program Instance embedCompose : Embed A C.
  Next Obligation.
(* Goal: @lentails C HC (@embed B C HE (@embed A B EmbOp p)) (@embed B C HE (@embed A B EmbOp q)) *)
  	do 2 apply embed_sound; assumption.
  Qed.
  Next Obligation.
  	split;
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	rewrite embedlforall; apply embed_sound; rewrite embedlforall; reflexivity.
  Qed.
  Next Obligation.
  	split;
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	rewrite embedlexists; apply embed_sound; rewrite embedlexists; reflexivity.
  Qed.
  Next Obligation.
  	split;
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	rewrite embedImpl; apply embed_sound; rewrite embedImpl; reflexivity.
  Qed.

End ILogicEmbedCompose.

Infix "/\\" := lembedand (at level 75, right associativity).
Infix "->>" := lembedimpl (at level 77, right associativity).

Section ILogicEmbedFacts.
  Context {A B} `{HAB: Embed A B} {ILA: ILogic A} {ILB: ILogic B}.

  Global Instance embed_lentails_m :
    Proper (lentails ==> lentails) embed.
  Proof.
(* Goal: @Proper (forall _ : A, B) (@respectful A B (@lentails A ILOpsA) (@lentails B ILOpsB)) (@embed A B EmbOp) *)
    intros a b Hab; apply embed_sound; assumption.
  Qed.

  Global Instance embed_lequiv_m :
    Proper (lequiv ==> lequiv) embed.
  Proof.
(* Goal: @Proper (forall _ : A, B) (@respectful A B (@lequiv A ILOpsA) (@lequiv B ILOpsB)) (@embed A B EmbOp) *)
    intros a b Hab; split; destruct Hab; apply embed_sound; assumption.
  Qed.

  Global Instance lembedimpl_lentails_m:
    Proper (lentails --> lentails ++> lentails) lembedimpl.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : B), B) (@respectful A (forall _ : B, B) (@flip A A Prop (@lentails A ILOpsA)) (@respectful B B (@lentails B ILOpsB) (@lentails B ILOpsB))) (@lembedimpl A B ILOpsB EmbOp) *)
    intros P P' HP Q Q' HQ; red in HP.
(* Goal: @lentails A ILOps C (@lembedimpl Prop A ILOps HPropOp p Q) *)
    unfold lembedimpl. rewrite <- HP, HQ; reflexivity.
  Qed.

  Global Instance lembedimpl_lequiv_m:
    Proper (lequiv ==> lequiv ==> lequiv) lembedimpl.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : B), B) (@respectful A (forall _ : B, B) (@lequiv A ILOpsA) (@respectful B B (@lequiv B ILOpsB) (@lequiv B ILOpsB))) (@lembedand A B ILOpsB EmbOp) *)
    intros P P' HP Q Q' HQ.
(* Goal: @lequiv B ILOpsB (@lembedimpl A B ILOpsB EmbOp P Q) (@lembedimpl A B ILOpsB EmbOp P' Q') *)
    split; apply lembedimpl_lentails_m; (apply HP || apply HQ).
  Qed.

  Global Instance lembedand_lentails_m:
    Proper (lentails ==> lentails ==> lentails) lembedand.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : B), B) (@respectful A (forall _ : B, B) (@lequiv A ILOpsA) (@respectful B B (@lequiv B ILOpsB) (@lequiv B ILOpsB))) (@lembedand A B ILOpsB EmbOp) *)
    intros P P' HP Q Q' HQ.
(* Goal: @lequiv A ILOps (@lembedand B A ILOps HEmbOp p (@lembedand Prop A ILOps HPropOpA P q)) (@lembedand Prop A ILOps HPropOpA P (@lembedand B A ILOps HEmbOp p q)) *)
    unfold lembedand. rewrite HP, HQ. reflexivity.
  Qed.

  Global Instance lembedand_lequiv_m:
    Proper (lequiv ==> lequiv ==> lequiv) lembedand.
  Proof.
(* Goal: @Proper (forall (_ : A) (_ : B), B) (@respectful A (forall _ : B, B) (@lequiv A ILOpsA) (@respectful B B (@lequiv B ILOpsB) (@lequiv B ILOpsB))) (@lembedand A B ILOpsB EmbOp) *)
    intros P P' HP Q Q' HQ.
(* Goal: @lequiv B ILOpsB (@lembedand A B ILOpsB EmbOp P Q) (@lembedand A B ILOpsB EmbOp P' Q') *)
    split; apply lembedand_lentails_m; (apply HP || apply HQ).
  Qed.

  Lemma embedland a b : embed a //\\ embed b -|- embed (a //\\ b).
  Proof.
    do 2 rewrite land_is_forall; rewrite <- embedlforall; split;
    apply lforallR; intro x; apply lforallL with x;
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    destruct x; reflexivity.
  Qed.

  Lemma embedlor a b : embed a \\// embed b -|- embed (a \\// b).
  Proof.
    do 2 rewrite lor_is_exists; erewrite <- embedlexists; split;
    apply lexistsL; intro x; apply lexistsR with x;
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    destruct x; reflexivity.
  Qed.

  Lemma embedlfalse : embed lfalse -|- lfalse.
  Proof.
    rewrite lfalse_is_exists; erewrite <- embedlexists; split;
    [apply lexistsL; intro x; destruct x | apply lfalseL].
  Qed.

  Lemma embedltrue : embed ltrue -|- ltrue.
  Proof.
    rewrite ltrue_is_forall; rewrite <- embedlforall; split;
    [apply ltrueR | apply lforallR; intro x; destruct x].
  Qed.

  Lemma embedlandC (P R : B) (Q : A) : P //\\ Q /\\ R -|- Q /\\ P //\\ R.
  Proof.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	unfold lembedand; rewrite <- landA, (landC P), landA; reflexivity.
  Qed.

  Lemma embedlimplC (P R : B) (Q : A) : P -->> Q ->> R -|- Q ->> P -->> R.
  Proof.
(* Goal: @lentails A ILOps C (@lembedimpl Prop A ILOps HPropOp p Q) *)
    unfold lembedimpl. do 2 rewrite limplAdj2.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    rewrite landC. reflexivity.
  Qed.

  Lemma limpllandC (P Q R : B) : P //\\ (Q -->> R) |-- Q -->> P //\\ R.
  Proof.
(* Goal: @lentails B ILOpsB (@land B ILOpsB P (@limpl B ILOpsB Q R)) (@limpl B ILOpsB Q (@land B ILOpsB P R)) *)
  	apply limplAdj; rewrite landA; apply landR.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	+ apply landL1. reflexivity.
  	+ apply landL2. apply limplL; [reflexivity | apply landL1; reflexivity].
  Qed.

  Lemma embed_existsL (P : A) : Exists x : |-- P, ltrue |-- embed P.
  Proof.
(* Goal: @lentails B ILOpsB (@lexists B ILOpsB (@lentails A ILOpsA (@ltrue A ILOpsA) P) (fun _ : @lentails A ILOpsA (@ltrue A ILOpsA) P => @ltrue B ILOpsB)) (@embed A B EmbOp P) *)
  	apply lexistsL; intro H.
(* Goal: @lentails B ILOpsB (@ltrue B ILOpsB) (@embed A B EmbOp P) *)
  	rewrite <- H. rewrite embedltrue. apply ltrueR.
  Qed.

End ILogicEmbedFacts.

Section EmbedProp.
  Context {A : Type} `{HIL: ILogic A} {HPropOp: EmbedOp Prop A} {HProp: Embed Prop A}.

  Lemma embedPropExists (p : Prop) : embed p |-- Exists x : p, ltrue.
  Proof.
    assert (p |-- Exists x : p, (|-- ltrue)). {
(* Goal: @lentails A ILOps P (@ltrue A ILOps) *)
      intros Hp. exists Hp. apply ltrueR.
    } etransitivity.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    rewrite H. reflexivity.
(* Goal: forall _ : p, @lentails A ILOps (@ltrue A ILOps) (@limpl A ILOps Q C) *)
    rewrite <- embedlexists. apply lexistsL. intros Hp.
(* Goal: @lentails A ILOps P (@ltrue A ILOps) *)
    apply lexistsR with Hp. apply ltrueR.
  Qed.

  Lemma embedPropExistsL (p : Prop) (P : A) : Exists x : p, P |-- embed p.
  Proof.
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
    assert (Exists x : p, ltrue |-- p). {
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
      intros HP. destruct HP as [HP _]. apply HP.
    }
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
    etransitivity; [|rewrite <- H]; [reflexivity|].
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop))) *)
    rewrite <- embedlexists. apply lexistsL; intro Hp.
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@ltrue B ILOps0)) C *)
    apply lexistsR with Hp. rewrite embedltrue. apply ltrueR.
  Qed.

  (* TODO rename embedPropExists to embedPropExistsR *)
  Lemma embedPropExists' (p : Prop) : Exists x : p, ltrue -|- embed p.
  Proof.
(* Goal: @lequiv A ILOps (@lexists A ILOps p (fun _ : p => @ltrue A ILOps)) (@embed Prop A HPropOp p) *)
  	split; [apply embedPropExistsL | apply embedPropExists].
  Qed.

  Lemma embedPropL (p : Prop) C (H: p -> |-- C) :
    embed p |-- C.
  Proof.
(* Goal: @lentails A ILOps (@embed Prop A HPropOpA P) (@embed B A HEmbOp (@embed Prop B HPropOpB P)) *)
(* Goal: @lentails A ILOps (@land A ILOps (@embed B A HEmbOp p) (@land A ILOps q (@embed Prop A HPropOpA P))) (@land A ILOps (@embed B A HEmbOp p) q) *)
  	rewrite embedPropExists.
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => @embed B A HEmbOp (@ltrue B ILOps0))) C *)
  	apply lexistsL; intro Hp.
(* Goal: @lentails A ILOps (@ltrue A ILOps) C *)
  	apply H; apply Hp.
  Qed.

  Lemma embedPropR (p : Prop) (P : A) (H : p) : P |-- embed p.
  Proof.
(* Goal: @lentails A ILOps P (@embed B A HEmbOp (@embed Prop B HPropOpB p)) *)
    assert (ltrue |-- p) by (intros _; assumption).
(* Goal: @lentails A ILOps P (@ltrue A ILOps) *)
    rewrite <- H0, embedltrue; apply ltrueR.
  Qed.

  Lemma lpropandL (p: Prop) Q C (H: p -> Q |-- C) :
    p /\\ Q |-- C.
  Proof.
(* Goal: @lequiv A ILOps (@lembedand B A ILOps HEmbOp p (@lembedand Prop A ILOps HPropOpA P q)) (@lembedand Prop A ILOps HPropOpA P (@lembedand B A ILOps HEmbOp p q)) *)
    unfold lembedand.
(* Goal: @lentails A ILOps (@land A ILOps (@embed Prop A HPropOp p) Q) C *)
    apply landAdj.
(* Goal: @lentails A ILOps (@embed Prop A HPropOp p) (@limpl A ILOps Q C) *)
    apply embedPropL.
(* Goal: forall _ : p, @lentails A ILOps (@ltrue A ILOps) (@limpl A ILOps Q C) *)
    intros Hp.
(* Goal: @lentails A ILOps (@land A ILOps (@limpl A ILOps (@embed Prop A HPropOpA P) q) (@embed B A HEmbOp p)) (@limpl A ILOps (@embed Prop A HPropOpA P) (@land A ILOps (@embed B A HEmbOp p) q)) *)
    apply limplAdj.
(* Goal: @lentails A ILOps (@land A ILOps q (@embed Prop A HPropOpA P)) (@embed B A HEmbOp (@embed Prop B HPropOpB P)) *)
(* Goal: @lentails A ILOps (@land A ILOps (@embed B A HEmbOp p) (@land A ILOps q (@embed Prop A HPropOpA P))) (@land A ILOps (@embed B A HEmbOp p) q) *)
    apply landL2.
(* Goal: @lentails A ILOps Q C *)
    apply H. assumption.
  Qed.

  Lemma lpropandR C (p: Prop) Q (Hp: p) (HQ: C |-- Q) :
    C |-- p /\\ Q.
  Proof.
(* Goal: @lequiv A ILOps (@lembedand B A ILOps HEmbOp p (@lembedand Prop A ILOps HPropOpA P q)) (@lembedand Prop A ILOps HPropOpA P (@lembedand B A ILOps HEmbOp p q)) *)
    unfold lembedand.
    apply landR; [|assumption].
(* Goal: @lentails A ILOps P (@ltrue A ILOps) *)
    rewrite <- embedPropR. apply ltrueR. assumption.
  Qed.

  Lemma lpropimplL (p: Prop) (Q C: A) (Hp: p) (HQ: Q |-- C) :
    p ->> Q |-- C.
  Proof.
(* Goal: @lentails A ILOps C (@lembedimpl Prop A ILOps HPropOp p Q) *)
    unfold lembedimpl.
(* Goal: P *)
    rewrite <- embedPropR, limplTrue; assumption.
  Qed.

  Lemma lpropimplR C (p: Prop) Q (H: p -> C |-- Q) :
    C |-- p ->> Q.
  Proof.
(* Goal: @lentails A ILOps C (@lembedimpl Prop A ILOps HPropOp p Q) *)
    unfold lembedimpl.
(* Goal: @lentails A ILOps (@land A ILOps (@embed B A HEmbOp p) (@limpl A ILOps (@embed Prop A HPropOpA P) q)) (@limpl A ILOps (@embed Prop A HPropOpA P) (@land A ILOps (@embed B A HEmbOp p) q)) *)
    apply limplAdj. rewrite landC. apply lpropandL. assumption.
  Qed.

  (* Derivable but useful *)
  Lemma lpropandTrue P : True /\\ P -|- P.
  Proof.
(* Goal: @lequiv A ILOps (@lembedand Prop A ILOps HPropOp False P) (@lfalse A ILOps) *)
    split.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    + apply lpropandL; intros _; reflexivity.
    + apply landR.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
      * replace True with (@ltrue Prop _) by reflexivity.
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@ltrue B ILOps0)) C *)
        rewrite embedltrue. apply ltrueR.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
      * reflexivity.
  Qed.

  Lemma lpropandFalse P : False /\\ P -|- lfalse.
  Proof.
(* Goal: @lequiv A ILOps (@lembedand Prop A ILOps HPropOp False P) (@lfalse A ILOps) *)
    split.
    + apply lpropandL; intros H; destruct H.
    + apply lfalseL.
  Qed.


End EmbedProp.


Section EmbedProp'.
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
  Context {A : Type} `{HILA: ILogic A} {HPropOpA: EmbedOp Prop A} {HPropA: Embed Prop A}.
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
  Context {B : Type} `{HILB: ILogic B} {HPropOpB: EmbedOp Prop B} {HPropB: Embed Prop B}.
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
  Context {HEmbOp : EmbedOp B A} {Hemb: Embed B A}.

  Lemma lpropandAL (p : B) (q : A) (P : Prop) : P /\\ p /\\ q |-- (P /\\ p) /\\ q.
  Proof.
(* Goal: @lentails A ILOps (@lembedand B A ILOps HEmbOp (@lembedand Prop B ILOps0 HPropOpB P p) q) (@lembedand Prop A ILOps HPropOpA P (@lembedand B A ILOps HEmbOp p q)) *)
    apply lpropandL; intros HP; apply landR.
    + apply landL1; apply embed_sound; apply landR.
(* Goal: P *)
      * apply embedPropR. assumption.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
      * reflexivity.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    + apply landL2; reflexivity.
  Qed.

  Lemma lpropandAC (p : B) (q : A) (P : Prop) : p /\\ P /\\ q -|- P /\\ p /\\ q.
  Proof.
(* Goal: @lequiv A ILOps (@lembedand B A ILOps HEmbOp p (@lembedand Prop A ILOps HPropOpA P q)) (@lembedand Prop A ILOps HPropOpA P (@lembedand B A ILOps HEmbOp p q)) *)
  	unfold lembedand. do 2 rewrite <- landA; rewrite (landC (embed p)); reflexivity.
  Qed.

  Lemma lpropandAR (p : B) (q : A) (P : Prop) : (P /\\ p) /\\ q |-- P /\\ p /\\ q.
  Proof.
(* Goal: @lentails A ILOps (@lembedand B A ILOps HEmbOp (@lembedand Prop B ILOps0 HPropOpB P p) q) (@lembedand Prop A ILOps HPropOpA P (@lembedand B A ILOps HEmbOp p q)) *)
  	apply landR.
  	+ apply landL1.
(* Goal: @lentails A ILOps (@lembedand B A ILOps HEmbOp (@lembedand Prop B ILOps0 HPropOpB P p) q) (@embed Prop A HPropOpA P) *)
  	  unfold lembedand; rewrite <- embedland; apply landL1.
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@embed Prop B HPropOpB p)) C *)
  	  rewrite embedPropExists, <- embedlexists.
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => @embed B A HEmbOp (@ltrue B ILOps0))) C *)
  	  apply lexistsL; intro Hp.
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@ltrue B ILOps0)) (@embed Prop A HPropOpA P) *)
  	  apply embedPropR; apply Hp.
  	+ unfold lembedand; rewrite <- embedland; apply landR.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	  * apply landL1; apply landL2. reflexivity.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
  	  * apply landL2; reflexivity.
 Qed.

 Lemma lpropimplAL (p : B) (q : A) (P : Prop) : (P ->> p) /\\ q |-- P ->> (p /\\ q).
 Proof.
(* Goal: @lentails A ILOps (@land A ILOps (@limpl A ILOps (@embed Prop A HPropOpA P) q) (@embed B A HEmbOp p)) (@limpl A ILOps (@embed Prop A HPropOpA P) (@land A ILOps (@embed B A HEmbOp p) q)) *)
    unfold lembedimpl, lembedand. apply limplAdj. rewrite landA.
(* Goal: @lentails A ILOps (@land A ILOps q (@embed Prop A HPropOpA P)) (@embed B A HEmbOp (@embed Prop B HPropOpB P)) *)
(* Goal: @lentails A ILOps (@land A ILOps (@embed B A HEmbOp p) (@land A ILOps q (@embed Prop A HPropOpA P))) (@land A ILOps (@embed B A HEmbOp p) q) *)
    rewrite <- embedImpl. apply limplL. apply landL2.
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => @embed B A HEmbOp (@ltrue B ILOps0))) C *)
    rewrite embedPropExists. apply lexistsL; intro Hp.
(* Goal: @lentails A ILOps (@ltrue A ILOps) (@embed B A HEmbOp (@embed Prop B HPropOpB P)) *)
(* Goal: @lentails A ILOps (@land A ILOps (@embed B A HEmbOp p) (@land A ILOps q (@embed Prop A HPropOpA P))) (@land A ILOps (@embed B A HEmbOp p) q) *)
    rewrite <- (embedPropR ltrue); [apply embedltrue | apply Hp].
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    apply landR; [apply landL1|apply landL2; apply landL1]; reflexivity.
 Qed.

 Lemma lpropimplAR (p : B) (q : A) (P : Prop) : p /\\ (P ->> q) |-- P ->> (p /\\ q).
 Proof.
(* Goal: @lentails A ILOps (@land A ILOps (@embed B A HEmbOp p) (@limpl A ILOps (@embed Prop A HPropOpA P) q)) (@limpl A ILOps (@embed Prop A HPropOpA P) (@land A ILOps (@embed B A HEmbOp p) q)) *)
    unfold lembedimpl, lembedand. rewrite landC. apply limplAdj. rewrite landA.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    apply limplL. apply landL2; reflexivity.
(* Goal: @lentails A ILOps (@embed B A HEmbOp p) (@embed B A HEmbOp p) *)
    apply landR; [apply landL2; apply landL1|apply landL1]; reflexivity.
 Qed.


  Lemma embedPropR2 (p : Prop) (P : A) (H : p) : P |-- embed (embed p).
  Proof.
(* Goal: @lentails A ILOps P (@embed B A HEmbOp (@embed Prop B HPropOpB p)) *)
    assert (ltrue |-- p) by (intros _; assumption).
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@ltrue B ILOps0)) C *)
    rewrite <- H0. do 2 rewrite embedltrue. apply ltrueR.
  Qed.

  Lemma embedPropL2 (p : Prop) (C : A) (H: p -> |-- C) :
    embed (embed p) |-- C.
  Proof.
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@embed Prop B HPropOpB p)) C *)
  	rewrite embedPropExists, <- embedlexists.
(* Goal: @lentails A ILOps (@embed B A HEmbOp (@ltrue B ILOps0)) C *)
  	apply lexistsL; intro Hp. rewrite embedltrue.
(* Goal: @lentails A ILOps (@ltrue A ILOps) C *)
  	apply H; apply Hp.
  Qed.

End EmbedProp'.

Section EmbedPropProp.

(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
Instance EmbedOpPropProp : EmbedOp Prop Prop := { embed := fun P => P }.
Instance EmbedPropProp : Embed Prop Prop.
Proof.
(* Goal: @Embed Prop ILogicOps_Prop Prop ILogicOps_Prop EmbedOpPropProp *)
  split; firstorder.
Qed.

End EmbedPropProp.

Section EmbedPropInj.
  Context {A : Type} `{ILA : ILogic A}.
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
  Context {EmbOp1 : EmbedOp Prop A} {Emb1 : Embed Prop A}.
(* Goal: @lentails Prop ILogicOps_Prop (@lexists Prop ILogicOps_Prop p (fun _ : p => @ltrue Prop ILogicOps_Prop)) p *)
(* Goal: @lentails A ILOps (@lexists A ILOps p (fun _ : p => P)) (@embed Prop A HPropOp p) *)
  Context {EmbOp2 : EmbedOp Prop A} {Emb2 : Embed Prop A}.

  Lemma emb_prop_eq (P : Prop) : @embed _ _ EmbOp1 P -|- @embed _ _ EmbOp2 P.
  Proof.
    split; rewrite embedPropExists; apply lexistsL; intro Hp;
      (rewrite <- (embedPropR ltrue); [apply ltrueR | apply Hp]).
  Qed.

End EmbedPropInj.
