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