proposition: Lemma env_sub_varDecl : forall E1 E2 p A, E1 [-] E2 |= p := A -> E1 |= p := A /\ E2 |= p :!.
proof: Proof. intros E F p A EFp. destruct (isVarDecl_dec F p) as [[B Fp] | Fp]. assert (EFn: E [-] F |= p :!). apply env_sub_ry with B; trivial. unfold VarD in *. inversion EFn; congruence. split; trivial. apply env_sub_suby_ly with F; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)