proposition: Lemma list_pred_zip_eq_rev : forall (A B : Set)(lsa : list A)(lsb : list B), (length lsa = length lsb) -> list_pred (fun p1 p2 => [a1, b1] <-2 p1; [b2, a2] <-2 p2; a1 = a2 /\ b1 = b2) (zip lsa lsb) (zip lsb lsa).
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *; try lia; econstructor. intuition. eauto. Qed.
imports: FCF.FCF Permutation