proposition: Lemma inv_trans : forall A (R : relation A) (P : A -> Prop), (forall a b, P a -> R a b -> P b) -> forall a b, P a -> trans_clos R a b -> P b.
proof: Proof. intros A R P Inv a b Pa a_Rp_b; induction a_Rp_b. apply Inv with x; trivial. apply IHa_Rp_b; apply Inv with x; trivial. Qed.
imports: Coq(Setoid Relations List Utf8)