proposition: Lemma functional_path A (s: relation A) (FUN: functional s): (s⁻¹)＊ ⨾ s＊ ⊆ s＊ ∪ (s⁻¹)＊.
proof: Proof. eapply rt_ind_left with (P:= fun __ => __ ⨾ s＊); relsf. intros k IH. rewrite !seqA, IH; relsf. apply inclusion_union_l. rewrite rt_begin at 1; relsf. apply inclusion_union_l; vauto. by rewrite functional_alt in FUN; sin_rewrite FUN; relsf. rewrite rt_begin at 2; relsf. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn