proposition: Lemma two_params_rule (bound i: nat) N phi psi (s1 s2 t : sty) : neutral normal_form N -> type_assignment (Γ_all bound i) N (arr s1 phi (arr s2 psi t)) -> (exists x (e : nat), N = var x /\ t = symbol e).
proof: Proof. move=> H. elim: H s1 phi s2 psi t. { move=> x > /type_assignmentE [] > /In_Γ_allE /[apply]. move=> [] // > [] *; subst; by eexists _, _. } move=> > ? IH ? > /type_assignmentE [] > /IH. firstorder 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