proposition: Lemma env_compose_morph_aux0 : forall El Er El' Er', (forall El El' Er', El [=] El' -> Er [=] Er' -> envSubset (El [+] Er) (El' [+] Er')) -> El [=] El' -> None :: Er [=] Er' -> envSubset (El [+] (None :: Er)) (El' [+] Er').
proof: Proof. set (env_subset_cons' := env_subset_cons); unfold decl in env_subset_cons'. intros. destruct Er'; destruct El; destruct El'; try destruct o; try destruct o0; try destruct o1; simpl; try solve [ exfalso; eapply env_eq_some_nil_absurd; eauto with terms | exfalso; eapply env_eq_some_none_absurd; eauto with terms | destruct H1; trivial ]; try apply env_subset_cons_none; trivial. rewrite (env_eq_empty_cons H1). rewrite <- (env_eq_empty_cons (env_eq_sym H0)). apply env_subset_refl. assert (None :: El[+]Er [=] EmptyEnv). apply env_eq_empty_cons_rev. split. change EmptyEnv with (EmptyEnv [+] EmptyEnv). apply H; apply env_eq_empty_cons; trivial. apply env_subset_empty. fold EmptyEnv; rewrite <- H2; apply env_subset_refl. rewrite (env_eq_cons_inv_hd H0). apply env_subset_cons'. replace El' with (El' [+] EmptyEnv). apply H; trivial. apply (env_eq_cons_inv H0). apply env_eq_empty_cons; trivial. rewrite env_sum_empty_r; trivial. replace El' with (El' [+] EmptyEnv). apply H; trivial. apply (env_eq_cons_inv H0). apply env_eq_empty_cons; trivial. rewrite env_sum_empty_r; trivial. apply env_subset_sum_r; destruct (env_eq_cons_inv H1); trivial. replace Er' with (nil [+] Er'). apply H; trivial. change (nil (A:=option SimpleType)) with (tail (None (A:=SimpleType) :: nil)) in H0. set (w := env_eq_tail H0); trivial. apply (env_eq_cons_inv H1). rewrite env_sum_empty_l; trivial. rewrite (env_eq_cons_inv_hd H0). apply env_subset_cons'. apply H. destruct (env_eq_cons_inv H0); fo. destruct (env_eq_cons_inv H1); fo. apply H. destruct (env_eq_cons_inv H0); fo. destruct (env_eq_cons_inv H1); fo. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)