fact: Fixpoint close {V} {o} (v: Vars (λ x, Term False (ne_list.one x)) V) (t: Term V o): Term False o := match t in Term _ o return Term False o with | Var x y => v y x | App _ x y z r => App _ x y (close v z) (close v r) | Op _ o => Op _ o end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic