proposition: Lemma trans_inversion : forall A (R : relation A) a b, trans_clos R a b -> (R a b \/ (exists c, trans_clos R a c /\ R c b)).
proof: Proof. intros A R a b H; induction H as [ a b H | a b c H H' [IH | IH]]. left; trivial. right; exists b; split; trivial; apply t_step; trivial. destruct IH as [d [H'' H''']]; right; exists d; split; trivial. apply trans_clos_is_trans with b; trivial; apply t_step; trivial. Qed.
imports: Coq(Setoid Relations List Utf8)