proposition: Lemma env_sub_suby_rn : forall E E' x A, E [-] E' |= x := A -> E' |= x :! .
proof: Proof. intros E E' x A EE'x. destruct (isVarDecl_dec E' x) as [[C E'x] | E'n]; trivial. exfalso; apply varD_UD_absurd with (E [-] E') x A; trivial. apply env_sub_ry with C; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)