fact: Fixpoint Arity (X:Type) (p : WFT X) (A : LRel X) := match p with | ZT _ => (forall ys, A ys <-> A nil) | SUP w => (forall x, Arity (w x) (fun ys => A (x::ys))) end.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)