fact: Definition rCompBeta s t := match s,t with |rCompClos (rLam ls) A,rCompClos (rLam lt) B => Some (rCompClos ls (t::A)) |rCompClos (rLam ls) A,rCompClos (rConst x) B => Some (rCompClos ls (t::A)) |rCompClos (rLam ls) A,rCompClos (rRho lt) B => Some (rCompClos ls (t::A)) |_,_ => None end.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd