proposition: Lemma s_rule_spec bound x s1 phi s2 psi a N : type_assignment (Γ_all bound bound) (var x) (arr s1 phi (arr s2 psi (symbol a))) -> normal_form N -> type_assignment (Γ_all bound bound) N s1 -> (exists r, In r rs /\ (forall i', nth_error (Γ_all bound i') x = Some (s_rule r))) /\ exists y, N = var y /\ y < bound /\ (forall i', nth_error (Γ_all bound i') y = Some (s_pos i' y)).
proof: Proof. move=> /type_assignmentE [>] /In_Γ_allE /[apply] Hx HN Hs1. split. { by case: Hx => // *; eexists; split; eassumption. } have {}HN : neutral normal_form N. { move: HN Hs1 => /normal_form_neutral []; first done. move=> [?] [-> ?]. move: Hx. by case=> // > [?????] _ _ => [| |_]; subst => /type_assignmentE. } case: HN Hs1. { move=> y Hy. exists y. split; first done. case: Hx Hy => // > [-> ????] _ _ => [| |_]. all: by move=> /type_assignmentE [>] /In_Γ_allE /[apply] - []. } move=> > []. { move=> ??. move: Hx. case=> // > [-> ????] _ _ => [| |_]. all: move=> /type_assignmentE [>] /type_assignmentE [>]. all: by move=> /In_Γ_allE /[apply] - []. } move=> > /two_params_rule H ??. move: Hx. case=> // > [-> ????] _ _ => [| |_]. all: move=> /type_assignmentE [>] /type_assignmentE [>]. all: by move=> /H [?] [?] []. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun