inlist_seq@{} (n : nat) x : InList x (seq n) <~> (x < n)%nat. Proof. simple_induction n n IHn. { symmetry; apply equiv_to_empty. apply not_lt_zero_r. } refine (_ oE equiv_transport _ (seq_succ _)). nrefine (_ oE (equiv_inlist_app _ _ _)^-1). nrefine (_ oE equiv_functor_sum' (B':=x = n) IHn _). 2: { simpl. exact (equiv_path_inverse _ _ oE sum_empty_r@{Set} _). } nrefine (_ oE equiv_leq_lt_or_eq^-1). rapply equiv_iff_hprop. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum