fact: Fixpoint map_var `(f: V → W) `(t: Term V o): Term W o := match t in Term _ o return Term W o with | Var v s => Var (f v) s | App _ _ _ x y => App _ _ _ (map_var f x) (map_var f y) | Op _ s => Op _ s end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic