proposition: Lemma completeness_init N : neutral normal_form N -> type_assignment (Γ_all 0 0) N hash -> type_assignment (Γ_all 0 1) N dollar -> exists N', normal_form N' /\ type_assignment (Γ_init ++ Γ_step) N' triangle.
proof: Proof. move=> ???. exists (app (var 0) N). split. { do ? constructor. by apply: neutral_normal_form. } apply: type_assignment_app. - econstructor; [done|]. by left. - done. - by constructor. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun