proposition: Lemma critical_pair1 (u v a : tm) of is_test a : dom ((u∥v°)·a) ≡ 1 ∥ u·a·v.
proof: Proof. by rewrite -dotA A10 cnvdot cnvtst partst. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)