proposition: Theorem Forall2_eq_refl : forall (A : Type)(ls : list A), Forall2 eq ls ls.
proof: Proof. induction ls; intuition idtac. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation