proposition: Lemma ct_inclusion_from_rt_inclusion2 A (r r': relation A) (d d' : A -> Prop) (ACYC : acyclic r) : ⦗d⦘ ⨾ r＊ ⊆ r'＊ ⨾ ⦗d'⦘ -> ⦗d⦘ ⨾ r⁺ ⊆ r'⁺ ⨾ ⦗d'⦘.
proof: Proof. rewrite !rtE; autounfold with unfolderDb; ins; desf. specialize (H z y); desf. assert (d' y /\ (z = y /\ True \/ r'⁺ z y)). { edestruct H; eauto. desf; eauto. } desf; eauto. exfalso; eapply ACYC; edone. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath