fact: Fixpoint eval u: X := match u with | sum i l => let o := Bin.value (e_bin i) in fold_map (fun un => let '(u,n):=un in @copy _ o n (eval u)) o l | prd i l => fold_map eval (Bin.value (e_bin i)) l | sym i v => eval_aux v (Sym.value (e_sym i)) | unit i => e_unit i end with eval_aux i (v: vT i): Sym.type_of i -> X := match v with | vnil => fun f => f | vcons _ u v => fun f => eval_aux v (f (eval u)) end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)