proposition: Theorem firstn_firstn : forall (A : Type)(ls : list A)(n1 n2 : nat), (n1 <= n2)%nat -> firstn n1 (firstn n2 ls) = firstn n1 ls.
proof: Proof. induction ls; destruct n1; destruct n2; intuition; simpl in *. lia. f_equal. eapply IHls. lia. Qed.
imports: FCF.FCF FCF.CompFold