proposition: Lemma env_eq_def : forall E1 E2, (forall i A, E1 |= i := A <-> E2 |= i := A) -> E1 [=] E2.
proof: Proof. induction E1. induction E2. intros; apply env_eq_refl. intros. destruct a. set (w := proj2 (H 0 s)); compute in w. set (p := w (eq_refl (Some (Some s)))); try_solve. apply env_eq_sym; apply env_eq_empty_cons_rev; apply env_eq_sym. apply IHE2; intros. split. destruct i; try_solve. intro D. set (w := proj2 (H (S i) A) D); try_solve. destruct E2; intros. apply env_eq_empty. intro j. destruct (isVarDecl_dec (a :: E1) j) as [[B D] | X]; trivial. set (w := proj1 (H j B) D). destruct j; try_solve. apply env_eq_cons. destruct a; destruct o; trivial. set (w := proj1 (H 0 s)); compute in w. set (p := w (eq_refl (Some (Some s)))); inversion p; trivial. set (w := proj1 (H 0 s)); compute in w. set (p := w (eq_refl (Some (Some s)))); inversion p. set (w := proj2 (H 0 s)); compute in w. set (p := w (eq_refl (Some (Some s)))); inversion p. apply IHE1. intros. set (hint := H (S i) A); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)