Commit e2e8748f by Jacques-Henri Jourdan

### eta-expand bi_mor_exist and bi_mor_forall.

parent 1f9e71cf
 ... ... @@ -2306,12 +2306,12 @@ Section bi_morphims. Global Instance bi_mor_mono_flip : Proper (flip (⊢) ==> flip (⊢)) mor. Proof. solve_proper. Qed. Lemma bi_mor_forall A Φ : mor (@bi_forall _ A Φ) ⊣⊢ (∀ x, mor (Φ x)). Lemma bi_mor_forall A (Φ : A → PROP1) : mor (∀ x, Φ x) ⊣⊢ (∀ x, mor (Φ x)). Proof. apply bi.equiv_spec; split; [|apply bi_mor_forall_2]. apply bi.forall_intro=>?. by rewrite bi.forall_elim. Qed. Lemma bi_mor_exist A Φ : mor (@bi_exist _ A Φ) ⊣⊢ (∃ x, mor (Φ x)). Lemma bi_mor_exist A (Φ : A → PROP1) : mor (∃ x, Φ x) ⊣⊢ (∃ x, mor (Φ x)). Proof. apply bi.equiv_spec; split; [apply bi_mor_exist_1|]. apply bi.exist_elim=>?. by rewrite -bi.exist_intro. ... ...
 ... ... @@ -342,8 +342,8 @@ Class BiMorphism {PROP1 PROP2 : bi} (f : PROP1 → PROP2) := { bi_mor_mono :> Proper ((⊢) ==> (⊢)) f; bi_mor_emp : f emp ⊣⊢ emp; bi_mor_impl_2 P Q : (f P → f Q)%I ⊢ f (P → Q)%I; bi_mor_forall_2 A Φ : (∀ x, f (Φ x)) ⊢ f (@bi_forall _ A Φ); bi_mor_exist_1 A Φ : f (@bi_exist _ A Φ) ⊢ ∃ x, f (Φ x); bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, f (Φ x)) ⊢ f (∀ x, Φ x); bi_mor_exist_1 A (Φ : A → PROP1) : f (∃ x, Φ x) ⊢ ∃ x, f (Φ x); bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x ≡ y) ⊢ (x ≡ y); bi_mor_sep P Q : f (P ∗ Q) ⊣⊢ (f P ∗ f Q); bi_mor_wand_2 P Q : (f P -∗ f Q) ⊢ f (P -∗ Q); ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!