proposition: Theorem In_gen_weaken : forall (A : Type)(e1 e2 : A -> A -> Prop) ls a, In_gen e1 a ls -> (forall a', e1 a a' -> e2 a a') -> In_gen e2 a ls.
proof: Proof. induction ls; intuition; simpl in *. intuition. Qed.
imports: List FCF.Fold FCF.RepeatCore