proposition: Lemma term_build_conv_sim : forall M M' N Q, M ~(Q) M' -> envSub_minimal Q M -> env M = env N -> envSubset (activeEnv N) (activeEnv M) -> exists N', env M' = env N' /\ N ~(Q) N'.
proof: Proof. intros M M' N Q MM' QMmin MNenv MNact. destruct (@term_build_conv N Q (env M')) as [Q' [Q'Q [N' [NN' [N'env [N'min _]]]]]]. intros. destruct (QMmin x y H). destruct (envSub_minimal_rev x y QMmin MM' H). set (M'y_x1 := activeEnv_subset M' H3). set (Mx_x0 := activeEnv_subset M H2). set (Mx_A := activeEnv_subset N H0). rewrite <- MNenv in Mx_A. destruct MM'. set (M'y_x0 := proj1 (H5 x y H x0) H2). inversion Mx_x0; inversion Mx_A. inversion H1; inversion M'y_x1. inversion M'y_x0; inversion H3. try_solve. assert (N'': env M' [+] dropEmptySuffix (env N') |- term N' := type N'). apply typing_ext_env_l. apply typing_drop_suffix. exact (typing N'). exists (buildT N''); split. simpl; rewrite N'min. rewrite term_env_activeEnv. rewrite env_sum_assoc. set (MQ'M' := terms_conv_extend_subst MM' Q'Q). set (N'M'aenv := terms_conv_activeEnv_sub MQ'M' MNact NN'). rewrite <- (@env_subset_as_sum_r (activeEnv M') (dropEmptySuffix (activeEnv N'))); trivial. apply env_subset_dropSuffix_length; trivial. apply env_subset_trans with (activeEnv N'); trivial. apply (proj1 (env_subset_dropSuffix_eq (activeEnv N'))). apply terms_conv_diff_env with N'; trivial. apply terms_conv_shrink_subst with Q'; trivial. intros. set (Mx := MNact x A H). exact (terms_conv_activeEnv MM' Mx). apply equiv_term_activeEnv; trivial. simpl. apply env_comp_dropSuffix. apply env_comp_ext_l. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)