proposition: Lemma Forall_nth_const v : Forall (fun i => nth i v 0 = 1) (seq 0 (length v)) -> v = repeat 1 (length v).
proof: Proof. elim: v; first done. move=> ? v IH /= /Forall_cons_iff [->]. by rewrite -seq_shift Forall_map => /IH <-. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun