proposition: Lemma stepISubst_expansion M N Gamma t : has_var_zero M -> type_assignment Gamma (subst (scons N var) M) t -> type_assignment Gamma (app (lam M) N) t.
proof: Proof. suff H : forall Gamma1 Gamma2, not (allfv (Nat.iter (length Gamma1) (scons True) is_nonzero) M) -> type_assignment (Gamma1 ++ Gamma2) (subst (Nat.iter (length Gamma1) (fun sigma => scons (var 0) (funcomp (ren S) sigma)) (scons N var)) M) t -> exists s_phi, type_assignment (Gamma1 ++ s_phi :: Gamma2) M t /\ type_assignment Gamma2 N (fst s_phi) /\ Forall (type_assignment Gamma2 N) (snd s_phi). { move=> HM /(H nil) [|[? ?]]. - move=> H'. apply: HM. apply: allfv_impl H'. by case. - move=> [?] [??]. econstructor; [|eassumption..]. by constructor. } move=> Gamma1 Gamma2. elim: M Gamma1 t. - move=> y Gamma1 t /= H. have <- : length Gamma1 = y. { elim: Gamma1 y H=> /=; [by case|]. move=> ?? IH [|y] /=; [done|]. by move=> /IH ->. } move=> HN. exists (t, nil). clear H. split; [|split; [|done]]. + econstructor; [|by left]. by rewrite nth_error_app2 ?Nat.sub_diag; [lia|]. + elim: Gamma1 HN; [done|]. move=> ? Gamma1 IH /= H. apply: IH. move: H=> /(type_assignment_ren_fv _ (Gamma1 ++ Gamma2) Nat.pred). rewrite !simpl_term. apply. apply: allfv_ren. by apply: allfv_trivial=> - [|?] /=. - move=> M1 + M2 + Gamma1 t. move=> /(_ Gamma1) + /(_ Gamma1). set P := (Nat.iter (length Gamma1) (scons True) is_nonzero). move=> IH1 IH2 H /=. have HP : forall n, Decidable.decidable (P n). { rewrite /P /Decidable.decidable /=. elim: (Gamma1) => /=. - case; by auto. - move=> ?? IH [|?] /=; by auto. } move=> /type_assignmentE [] s' phi'. have := allfv_dec _ M2 HP. have := allfv_dec _ M1 HP. move=> [|] HM1 [|] HM2. + move: H=> /=. tauto. + move: HM1 => /type_assignment_allfv_substE /[apply] H'M1. move=> /(IH2 _ HM2) [[s2 phi2]] [?] [??]. move=> /(@Forall_impl _ _ _ (fun t => IH2 t HM2)). move=> /Forall_exists_Forall2 [tys] Hphi'. exists (s2, (phi2 ++ concat (map (fun '(s', phi') => s' :: phi') tys))). split; [|split]. * econstructor. ** by apply: H'M1. ** apply: type_assignment_weaken_assumption; [|by eassumption]. move=> ?. do ? rewrite /= in_app_iff; tauto. ** move: Hphi'. elim; [done|]. move=> ? [??] > /= [?] [??] _ H'. constructor. *** apply: type_assignment_weaken_assumption; [|by eassumption]. move=> ?. do ? rewrite /= in_app_iff; tauto. *** apply: Forall_impl H' => ?. apply: type_assignment_weaken_assumption. move=> ?. do ? rewrite /= in_app_iff; tauto. * by eassumption. * apply /Forall_app. split; [by eassumption|]. apply /Forall_concat /Forall_map. elim: Hphi'; [done|]. move=> ? [??] > [_] /= [??] *. by do ? constructor. + move=> /(IH1 _ HM1) [[s phi]] [?] [??] H1M2 H2M2. exists (s, phi). split; [|by split]. econstructor. * by eassumption. * by apply: type_assignment_allfv_substE; eassumption. * apply: Forall_impl H2M2 => ?. by apply: type_assignment_allfv_substE. + move=> /(IH1 _ HM1) [[s1 phi1]] [?] [??]. move=> /(IH2 _ HM2) [[s2 phi2]] [?] [??]. move=> /(@Forall_impl _ _ _ (fun t => IH2 t HM2)). move=> /Forall_exists_Forall2 [tys] Hphi'. exists (s1, (phi1 ++ s2 :: phi2 ++ concat (map (fun '(s', phi') => s' :: phi') tys))). split; [|split]. * econstructor. ** apply: type_assignment_weaken_assumption; [|by eassumption]. move=> ?. do ? rewrite /= in_app_iff; tauto. ** apply: type_assignment_weaken_assumption; [|by eassumption]. move=> ?. do ? rewrite /= in_app_iff; tauto. ** move: Hphi'. elim; [done|]. move=> ? [??] > [?] [??] _ H'. constructor. *** apply: type_assignment_weaken_assumption; [|by eassumption]. move=> ?. do ? rewrite /= in_app_iff; tauto. *** apply: Forall_impl H' => ?. apply: type_assignment_weaken_assumption. move=> ?. do ? rewrite /= in_app_iff; tauto. * eassumption. * apply /Forall_app. split; [done|]. apply: Forall_cons; [done|]. apply /Forall_app. split; [done|]. elim: Hphi'; [done|]. move=> ? [??] > /= [?] [??] _ ?. by constructor; [|apply /Forall_app]. - move=> M IH Gamma1 [?|s' phi' t] /= HM /type_assignmentE; [done|]. move=> /(IH ((s', phi') :: Gamma1)) {}IH. move: IH => [|[s phi]]. { move=> H. apply: HM. apply: allfv_impl H. by case. } move=> [?] [??]. exists (s, phi). by do 2 constructor. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect