proposition: Lemma soundness_init (N : term) : neutral normal_form N -> type_assignment (Γ_init ++ Γ_step) N triangle -> exists (N' : term), neutral normal_form N' /\ type_assignment (Γ_all 0 0) N' hash /\ type_assignment (Γ_all 0 1) N' dollar.
proof: Proof. case. { move=> x /type_assignmentE [>] /(In_Γ_allE 0 0) /[apply]. by case. } move=> ? N' []; first last. { move=> > /two_params_rule H ??. move=> /type_assignmentE [>] /type_assignmentE [>]. by move=> /(H 0 0) [?] [?] []. } move=> ?? /type_assignmentE [>] /type_assignmentE [>] /(In_Γ_allE 0 0) /[apply]. case=> //. move=> [-> ->] ? ? /Forall_cons_iff [? _]. exists N'. split; last done. apply: nf_hf_atom; by 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