proposition: Lemma env_sub_suby_ly : forall E E' x A, E [-] E' |= x := A -> E |= x := A.
proof: Proof. intros E E' x A EE'x. destruct (isVarDecl_dec E x) as [[B Ex] | En]. set (E'n := env_sub_suby_rn E E' EE'x). set (w := env_sub_ly_rn Ex E'n). assert (A = B). unfold VarD in *; congruence. rewrite H; trivial. set (w := env_sub_ln E' En). inversion w; unfold VarD in EE'x; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)