proposition: Lemma completeness (m : nat) : multi_step rs (repeat 0 (1+m)) (repeat 1 (1+m)) -> exists N, normal_form N /\ type_assignment (Γ_init ++ Γ_step) N triangle.
proof: Proof. have unnest : forall (A B C : Prop), A -> (B -> C) -> (A -> B) -> C by auto. move=> /completeness_star => /(_ (var (m + 3))). apply: (unnest). { move=> ?. rewrite nth_repeat. apply /in_app_iff. right. by left. } apply: (unnest). { by constructor. } apply: (unnest). { rewrite repeat_length. lia. } apply: (unnest). { by econstructor; [rewrite In_Γ_all_skip_lr|by left]. } apply: (unnest). { apply /Forall_forall => ??. by econstructor; [rewrite In_Γ_all_skip_lr|by left]. } move=> [N'] [+] [+] HN' => /completeness_0 /[apply]. apply: (unnest). { move: HN'. have -> : m + 1 = S m by lia. apply: Forall_impl => ?. by rewrite nth_repeat. } move=> [N''] [+] [+] [+] => /completeness_expand /[apply] /[apply] /[apply]. move=> [N'''] [?] [?] ?. by apply: completeness_init; eassumption. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun