fact: Definition rComp_ind_deep' (P : rComp -> Prop) (Pl : list rComp -> Prop) (IHVar : forall x : nat, P (rCompVar x)) (IHApp : forall s : rComp, P s -> forall t : rComp, P t -> P (s t)) (IHClos : forall (s : rTerm) (A : list rComp), Pl A -> P (rCompClos s A)) (IHNil : Pl nil) (IHCons : forall (a:rComp) (A : list rComp), P a -> Pl A -> Pl (a::A)) (x:rComp) : P x := (fix f c : P c:= match c with | rCompVar x => IHVar x | rCompApp s t => IHApp s (f s) t (f t) | rCompClos s A => IHClos s A ((fix g A : Pl A := match A with [] => IHNil | a::A => IHCons a A (f a) (g A) end) A) end) x .
imports: Undecidability.L.Tactics(LClos) ZArith FunInd