proposition: Theorem In_gen_equiv_compat : forall (ls : list A)(a1 a2 : A), ea a1 a2 -> In_gen a1 ls -> In_gen a2 ls.
proof: Proof. induction ls; intuition; simpl in *. intuition. left. eapply ea_trans. eapply ea_symm. eauto. trivial. right. eauto. Qed.
imports: List FCF.Fold