proposition: Lemma env_sum_varDecl : forall E1 E2 p A, E1 [+] E2 |= p := A -> {E1 |= p := A /\ E2 |= p :!} + {E2 |= p := A}.
proof: Proof. intros E F p A EFp. destruct (isVarDecl_dec F p) as [[B Fp] | Fn]. right. set (w := env_sum_ry E Fp). assert (A = B). unfold VarD in *; congruence. rewrite H; trivial. left; split; trivial. destruct (isVarDecl_dec E p) as [[B Ep] | En]. set (w := env_sum_ly_rn Ep Fn). assert (A = B). unfold VarD in *; congruence. rewrite H; trivial. set (w := env_sum_ln_rn En Fn). inversion w; unfold VarD in EFp; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)