proposition: Lemma env_compose_morph_aux : forall El Er El' Er', El [=] El' -> Er [=] Er' -> envSubset (El [+] Er) (El' [+] Er').
proof: Proof. set (env_subset_cons' := env_subset_cons); unfold decl in env_subset_cons'. intros El Er; gen El; induction Er; clear El. intros. rewrite env_sum_empty_r. apply env_subset_sum_l. rewrite <- H0. apply env_comp_empty. destruct H; trivial. intros; destruct a; destruct Er'. exfalso; eapply env_eq_some_nil_absurd; eauto. destruct o. rewrite (env_eq_cons_inv_hd H0); rewrite (env_eq_cons_inv_hd H0) in H0. destruct (env_eq_cons_inv H0). destruct El; destruct El'; try destruct o; try destruct o0; simpl; apply env_subset_cons'; try solve [ exfalso; eapply env_eq_some_nil_absurd; eauto with terms | apply IHEr; eapply env_eq_cons_inv; eauto | exfalso; eapply env_eq_some_none_absurd; eauto with terms | trivial ]. apply env_subset_sum_r; destruct (env_eq_cons_inv H0); trivial. replace Er' with (nil [+] Er'). apply IHEr; trivial. change (nil (A:=option SimpleType)) with (tail (None (A:=SimpleType) :: nil)) in H. set (w := env_eq_tail H); trivial. fo. rewrite env_sum_empty_l; trivial. exfalso; eapply env_eq_some_none_absurd; eauto with terms. apply env_compose_morph_aux0; trivial. apply env_compose_morph_aux0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)