proposition: Lemma env_subset_as_sum_r : forall E E', length E' <= length E -> envSubset E' E -> E = E [+] E'.
proof: Proof. induction E. intros; inversion H; destruct E'; try_solve. intros. destruct E'; trivial. assert (E = E [+] E'). apply (IHE E'). simpl in H; lia. apply env_subset_cons_rev with o a; trivial. assert (forall E E' (a: option SimpleType), E = E' -> a :: E = a :: E'). intros; replace E0 with E'0; trivial. destruct a; destruct o; simpl; try solve [apply H2; trivial]. replace s with s0. apply H2; trivial. assert ((Some s0 :: E') |= 0 := s0). constructor. set (w := H0 0 s0 H3); inversion w; trivial. exfalso; apply varD_UD_absurd with (None::E) 0 s. apply H0; constructor. right; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)