proposition: Lemma envSub_min_ex : forall M N Q, M ~(Q) N -> exists Q', M ~(Q') N /\ envSub_minimal Q' M /\ Q |=> Q'.
proof: Proof. destruct M as [E Pt T M]; induction M; intros; destruct H; inversion H; term_inv N; unfold Tr. exists (singletonEnvSubst x y); split. constructor. inversion H2. simpl; rewrite <- H6. constructor; simpl; auto. apply conv_env_var with x y; try solve [simpl; auto]. apply terms_conv_eq_type; exists Q; constructor; trivial. split. intros p q pq. inversion pq. rewrite H5. exists A; simpl; unfold VarD, EmptyEnv, decl. apply nth_after_copy. intros p q pq. inversion pq. rewrite H5; rewrite H6; trivial. exists emptyEnvSubst; repeat split; try_solve; try solve [intros x y xy; inversion xy]. rewrite H3; constructor. destruct (IHM (buildT T) (envSubst_lift1 Q)) as [Q' [MT [Q'min QQ']]]. change (buildT M) with (absBody (M:=buildT (TAbs M)) I). change (buildT T) with (absBody (M:=buildT (TAbs T)) I). apply abs_conv_absBody_aux; constructor; trivial. destruct (envSubst_add Q' 0 0) as [Q'' [Q''Q' [Q''00 Q''ext]]]. destruct (envSub_dec Q' 0 0). left; trivial. right; split; intro. destruct x; try_solve. absurd (0 = Datatypes.S x). lia. apply envSub_Lok with (envSubst_lift1 Q) 0. destruct Q; simpl; trivial. apply QQ'; trivial. destruct x; try_solve. absurd (Datatypes.S x = 0). lia. apply envSub_Rok with (envSubst_lift1 Q) 0. apply QQ'; trivial. destruct Q; simpl; trivial. exists (envSubst_lower Q''); split. apply abs_conv with I I. inversion H4; trivial. simpl. rewrite (envSubst_lift_lower Q'' Q''00); trivial. apply terms_conv_extend_subst with Q'; trivial. split. intros p q pq. destruct (Q''ext (Datatypes.S p) (Datatypes.S q)). destruct Q''; simpl; trivial. destruct (Q'min (Datatypes.S p) (Datatypes.S q) H6). exists x. rewrite (activeEnv_abs (buildT (TAbs M)) I). apply varD_tail; trivial. inversion H6; try_solve. apply envSubst_lift1_ext_rev. rewrite (envSubst_lift_lower Q'' Q''00); trivial. intros p q pq. destruct (Q''ext p q pq). apply QQ'; trivial. destruct H6; rewrite H6; rewrite H7. destruct Q; simpl; trivial. destruct (IHM1 (buildT T1) Q) as [Q'l [MTl [Q'l_min QQ'l]]]. change (buildT M1) with (appBodyL (M:=buildT (TApp M1 M2)) I). change (buildT T1) with (appBodyL (M:=buildT (TApp T1 T2)) I). apply app_conv_app_left_aux; constructor; trivial. destruct (IHM2 (buildT T2) Q) as [Q'r [MTr [Q'r_min QQ'r]]]. change (buildT M2) with (appBodyR (M:=buildT (TApp M1 M2)) I). change (buildT T2) with (appBodyR (M:=buildT (TApp T1 T2)) I). apply app_conv_app_right_aux; constructor; trivial. exists (sumEnvSubst QQ'l QQ'r); split. apply app_conv with I I; simpl. apply terms_conv_extend_subst with Q'l; trivial. apply sumEnvSubst_ext_l. apply terms_conv_extend_subst with Q'r; trivial. apply sumEnvSubst_ext_r. split. intros p q pq. destruct (sumEnvSubst_or pq). destruct (Q'l_min p q H7). exists x. apply (activeEnv_appBodyL_varD (buildT (TApp M1 M2)) I H8). destruct (Q'r_min p q H7). exists x. apply (activeEnv_appBodyR_varD (buildT (TApp M1 M2)) I H8). apply sumEnvSubst_ext. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)