proposition: Lemma clos_trans_restr_trans_mid : forall X (r r' : relation X) f x y (A : (restr_rel f (r ∪ r'))⁺ x y) z (B : r y z) w (C : (restr_rel f (r ∪ r'))⁺ z w), (restr_rel f (r ∪ r'))⁺ x w.
proof: Proof. ins; eapply t_trans, t_trans; vauto. eapply t_step; repeat split; vauto. by apply clos_trans_restrD in A; desc. by apply clos_trans_restrD in C; desc. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath