proposition: Lemma ct_inclusion_from_rt_inclusion1 A (r r': relation A) (d d' : A -> Prop) (ACYC : acyclic r) : r＊ ⨾ ⦗d⦘ ⊆ ⦗d'⦘ ⨾ r'＊ -> r⁺ ⨾ ⦗d⦘ ⊆ ⦗d'⦘ ⨾ r'⁺.
proof: Proof. rewrite !rtE; autounfold with unfolderDb; ins; desf. specialize (H x y); desf. assert (d' x /\ (x = y /\ True \/ r'⁺ x 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