proposition: Theorem soundness N : normal_form N -> type_assignment (Γ_init ++ Γ_step) N triangle -> exists (m : nat), multi_step rs (repeat 0 (1+m)) (repeat 1 (1+m)).
proof: Proof. move=> /nf_hf_atom + /[dup] => /[apply]. move=> /soundness_init /[apply] - [N'] [] + []. move=> /(soundness_expand 0) /[apply] /[apply] => /(_ (Forall_nil _)). move=> [bound] [N''] [] /soundness_step H H'. exists bound. move: H'. have -> : 1 + bound = bound + 1 by lia. move=> H'. apply: H. { by rewrite repeat_length. } move: H' => /Forall_map. apply: Forall_impl => i. by rewrite nth_repeat. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun