proposition: Lemma env_sub_ly_rn : forall E E' x A, E |= x := A -> E' |= x :! -> E [-] E' |= x := A.
proof: Proof. induction E; destruct E' as [|a' E']; intros; try solve [inversion H; destruct x; simpl in *; discr]. simpl; destruct a; trivial. destruct x. destruct a; destruct a'; unfold VarD in *; inversion H0; simpl in *; solve [discr | trivial]. inversion H. simpl; destruct a; destruct a'; unfold VarD; simpl; apply IHE; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)