fact: Fixpoint eval (u: term): X := match u with | tm_dot u v => eval u · eval v | tm_par u v => eval u ∥ eval v | tm_cnv u => (eval u) ° | tm_dom u => dom (eval u) | tm_one => 1 | tm_top => top | tm_var a => f a end.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures pttdom)