proposition: Lemma nth_error_seq start len n : n < len -> nth_error (seq start len) n = Some (start+n).
proof: Proof. elim: len start n. { lia. } move=> len IH start [|n] ?. { congr Some. lia. } rewrite /= IH; [|congr Some]; lia. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect