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