proposition: Lemma env_sum_right : forall E1 E2 x A1 A2, E1 |= x := A1 -> E2 [+] E1 |= x := A2 -> A1 = A2.
proof: Proof. induction E1; destruct E2; destruct x; unfold VarD; try_solve; try congruence. intros A1 A2 aA1. inversion aA1; congruence. intros A1 A2 E1x. destruct a; intro H; apply IHE1 with E2 x; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)