proposition: Lemma qo_clos_inv : forall t u, qo_clos R t u -> E t u \/ exists v, R t v /\ qo_clos R v u.
proof: Proof. induction 1. right. ex y. intuition. auto. destruct IHqo_clos1 as [h1|[a [i1 i2]]]; destruct IHqo_clos2 as [h2|[b [j1 j2]]]. left. trans y; hyp. right. ex b. rewrite h1. auto. right. ex a. rewrite <- h2. auto. right. ex a. intuition. trans b. trans y. hyp. apply qo_step. hyp. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)