proposition: Lemma list_pred_length_eq : forall (A B : Set)(lsa : list A)(lsb : list B)(P : A -> B -> Prop), list_pred P lsa lsb -> length lsa = length lsb.
proof: Proof. induction 1; intuition; simpl in *. f_equal. intuition. Qed.
imports: FCF.FCF