proposition: Lemma completeness_expand bound N : neutral normal_form N -> Forall (fun (i : nat) => type_assignment (Γ_all bound i) N star) (seq 1 bound) -> type_assignment (Γ_all bound 0) N hash -> type_assignment (Γ_all bound (1 + bound)) N dollar -> exists N', neutral normal_form N' /\ type_assignment (Γ_all 0 0) N' hash /\ type_assignment (Γ_all 0 1) N' dollar.
proof: Proof. elim: bound N. { move=> *. eexists. by split; [eassumption|]. } move=> bound IH N HN H1N H2N H3N. apply: (IH (app (var (bound + 1)) (lam N))). - do ? constructor. by by apply: neutral_normal_form. - move: H1N => /= /Forall_cons_iff [_]. rewrite -!seq_shift !map_map => /Forall_map H'N. apply /Forall_map. apply: Forall_impl H'N => ? H'N. apply: type_assignment_app. + econstructor; [by rewrite In_Γ_all_skip_lr|]. by left. + do ? constructor. move: H'N. by rewrite /Γ_all /= -seq_shift map_map. + done. - apply: type_assignment_app. + econstructor; [by rewrite In_Γ_all_skip_lr|]. right. by left. + do ? constructor. move: H1N => /Forall_cons_iff [+ _]. by rewrite /Γ_all /= -seq_shift map_map. + done. - apply: type_assignment_app. + econstructor; [by rewrite In_Γ_all_skip_lr|]. right. right. by left. + do ? constructor. move: H2N. by rewrite /Γ_all /= -seq_shift map_map Γ_lr_bound_S. + do ? constructor. move: H3N. by rewrite /Γ_all /= -seq_shift map_map. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun