proposition: Lemma completeness_star (bound : nat) (N : term) (v : list nat) : multi_step rs v (repeat 1 (1+bound)) -> (forall i, In (nth i v 0) symbols) -> neutral normal_form N -> length v = bound + 1 -> type_assignment (Γ_all bound (1 + bound)) N (symbol 1) -> Forall (fun i => type_assignment (Γ_all bound i) N (symbol 1)) (seq 0 (bound + 1)) -> exists N', neutral normal_form N' /\ type_assignment (Γ_all bound (1 + bound)) N' (symbol 1) /\ Forall (fun i => type_assignment (Γ_all bound i) N' (symbol (nth i v 0))) (seq 0 (bound + 1)).
proof: Proof. move=> /clos_rt_rt1n_iff. move E: (repeat 1 (1+bound)) => w Hvw. elim: Hvw E N; clear v w. { move=> ? <- N ??? HN. exists N. split; [done|split;[done|]]. apply: Forall_In_impl H => i /in_seq ?. congr type_assignment. congr symbol. rewrite (nth_indep _ 0 1). { rewrite repeat_length. lia. } by rewrite nth_repeat. } move=> v u w /[dup] /step_length_eq Hvu /[dup] /step_symbols H'vu. move=> /completeness_step H _ /[apply] + N /[dup] Hv /H'vu ++ /[dup] H'v. rewrite Hvu. do 5 move=> /[apply]. move=> [N'] [?] [? ?]. by apply: H; 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