proposition: Lemma term_build_conv_rel : forall M N N' Q, envSubset (activeEnv N) (activeEnv M) -> N ~(Q) N' -> envSub_minimal Q N -> exists Q', Q' |=> Q /\ exists M', M ~(Q') M' /\ envSubset (env N') (env M').
proof: Proof. intros. destruct (@term_build_conv M Q (env N')) as [Q' [Q'Q [M' [MM' [Nenv Mmin]]]]]. intros. destruct (envSub_minimal_rev x y H1 H0 H2). set (N'y := activeEnv_subset N' H5). set (Nenv_conv := proj2 H0 x y H2 x0). set (Nx := (proj2 Nenv_conv) H5). set (Mx := H x x0 Nx). inversion H3; inversion Mx. inversion N'y; inversion H4; try_solve. exists Q'; split; trivial. assert (M'': env N' [+] env M' |- term M' := type M'). apply typing_ext_env_l; exact (typing M'). exists (buildT M''); split. apply terms_conv_diff_env with M'; trivial. apply equiv_term_activeEnv; trivial. simpl; apply env_comp_ext_l. simpl; apply env_subset_sum_l. apply env_comp_sym; trivial. apply env_subset_refl. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)