proposition: Lemma normal_iso (s t: nterm): tgraph_of_nterm s ≃2p tgraph_of_nterm t -> term_of_nterm s ≡ term_of_nterm t.
proof: Proof. case s=>[a|a u b]; case t=>[c|c v d]=>/=; move=> [[h hi ho]]. - symmetry. by apply (vlabel_iso h tt). - exfalso. generalize (bijK' h (inl tt)). generalize (bijK' h (inr tt)). case (h^-1 (inr tt)). case (h^-1 (inl tt)). congruence. - exfalso. generalize (bijK h (inl tt)). generalize (bijK h (inr tt)). case (h (inr tt)). case (h (inl tt)). congruence. - generalize (vlabel_iso h (inl tt)). generalize (vlabel_iso h (inr tt)). simpl in *. rewrite hi ho /=. generalize (elabel_iso h None). generalize (endpoint_iso h (h.d None) None). have H: h.e None = None by case (h.e None)=>//; repeat case. rewrite H. case (iso_d h None)=>/=. by rewrite hi. intros. symmetry. apply dot_eqv=>//. apply dot_eqv=>//. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) GraphTheory(setoid_bigop structures mgraph pttdom mgraph2) GraphTheory(rewriting reduction open_confluence transfer)