take_length_leq@{i|} {A : Type@{i}} (n : nat) (l : list A) (H : (length l <= n)%nat) : take n l = l. Proof. induction l as [|a l IHl] in H, n |- * using list_ind@{i i}. 1: apply take_nil. destruct n. 1: destruct (not_lt_zero_r _ H). cbn; f_ap. by apply IHl, leq_pred'. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum