length_take@{i|} {A : Type@{i}} (n : nat) (l : list A) : length (take n l) = nat_min n (length l). Proof. induction l as [|a l IHl] in n |- * using list_ind@{i i}. { rewrite take_nil. rewrite nat_min_r. 1: reflexivity. cbn; exact _. } destruct n. 1: reflexivity. cbn; f_ap. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum