proposition: Lemma conv_subst_singleton_build M M' T G Q : envSub Q 0 0 -> M ~(Q) M' -> envSub_minimal Q M -> isSingletonSubst T G -> correct_subst M G -> exists Q' G' T', correct_subst M' G' /\ isSingletonSubst T' G' /\ Q' |=> Q /\ G ~~(Q') G'.
proof: Proof. intros. destruct (@term_build_conv T Q (None :: tail (env M'))) as [Q' [Q'Q [T' [TT' [T'env T'min]]]]]. intros. destruct x; destruct y. inversion H6. absurd (0 = S y); [lia | apply envSub_Lok with Q 0; trivial]. absurd (S x = 0); [lia | apply envSub_Rok with Q 0; trivial]. destruct (envSub_minimal_rev (S x) (S y) H1 H0 H4). replace B with x0. set (MM'comp := proj2 H0 (S x) (S y) H4). set (w := proj2 (MM'comp x0) H7). set (Tx := activeEnv_subset T H5). set (Mx := activeEnv_subset M w). apply (@ran_c M G H3 (S x)); trivial. rewrite (subst_ran_singleton H2). apply env_sub_ly_rn; trivial. destruct (subst_dom_singleton H2) as [E [Gdom Eempty]]. rewrite Gdom; unfold VarUD; simpl. destruct (Eempty x); auto. assert (M'y := activeEnv_subset M' H7); clear H7. inversion H6; inversion M'y; destruct (env M'); try_solve. exists Q'; exists (Some T'::nil); exists T'; split. constructor. apply subst_envs_comp_single. intros p A B T'p M'p. destruct p. inversion T'p. rewrite <- (terms_conv_eq_type (conv_by TT')). apply (@dom_c M G H3 0). destruct (subst_dom_singleton H2) as [E [DomG Eempty]]. rewrite DomG; constructor. apply activeEnv_subset. destruct (envSub_minimal_rev 0 0 H1 H0 H). inversion H0. set (M'0 := proj2 (H7 0 0 H x) H4). set (w := activeEnv_subset M' H4). assert (x = B). inversion w; inversion M'p; try_solve. rewrite <- H8; trivial. inversion T'p; destruct p; try_solve. rewrite subst_ran_single. intros p A B T'ps M'p. destruct p. destruct (env T'); try destruct o; try_solve. apply (T'env (S p)). apply (env_sub_suby_ly (env T') (subst_dom {x/T'})); trivial. inversion M'p; destruct (env M'); try_solve. split. apply singletonSubst_cond. split; trivial. apply singletonSubst_conv_rev with T T'; trivial. apply singletonSubst_cond. apply Q'Q; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)