proposition: Theorem list_pred_I_in : forall (A B : Set)(lsa : list A)(lsb : list B), length lsa = length lsb -> list_pred (fun a b => In a lsa /\ In b lsb) lsa lsb.
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *. econstructor. discriminate. discriminate. econstructor. intuition. eapply list_pred_impl. eapply IHlsa. lia. intuition. intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation