proposition: Lemma list_pred_I : forall (A B : Set)(lsa : list A)(lsb : list B), (length lsa = length lsb) -> list_pred (fun a b => True) lsa lsb.
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *; try lia. econstructor. econstructor; intuition. Qed.
imports: FCF.FCF