proposition: Lemma completeness_0 bound N : neutral normal_form N -> Forall (fun (i : nat) => type_assignment (Γ_all bound i) N (symbol 0)) (seq 0 (S bound)) -> type_assignment (Γ_all bound (1 + bound)) N (symbol 1) -> exists 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.
proof: Proof. move=> ? /= /Forall_cons_iff [H1N H2N] H3N. exists (app (var (bound + 2)) N). do ? split. - do ? constructor. by apply: neutral_normal_form. - apply: Forall_impl H2N => ? ?. apply: type_assignment_app. + econstructor; [by rewrite In_Γ_all_skip_lr|]. by left. + done. + done. - apply: type_assignment_app. + econstructor; [by rewrite In_Γ_all_skip_lr|]. right. by left. + done. + done. - apply: type_assignment_app. + econstructor; [by rewrite In_Γ_all_skip_lr|]. right. right. by left. + done. + done. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun