proposition: Lemma forall_weak (H: Transitive R): forall (l:list A) (a b:A), R a b -> List.Forall (R b) l -> List.Forall (R a) l.
proof: Proof. Proof with auto. induction 2. - constructor. - constructor ... transitivity b... Qed.
imports: hydras(DecPreOrder_Instances)