proposition: Theorem completeness (u v: term): graph_of_term u ≃2p graph_of_term v -> u ≡ v.
proof: Proof. move=>/tgraph_graph_iso h. pose proof (reduce u) as H. have H' : steps (tgraph_of_term u) (tgraph_of_nterm (nt v)) by rewrite h; apply reduce. case (confluence H H')=>F [/normal_steps HF /normal_steps HF']. rewrite-> (nt_correct u), (nt_correct v). apply normal_iso. by rewrite HF'. 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)