Full polyadic in Idris

Polyadic.idr

module Polyadic

import Data.Vect

parameters (o : Nat -> Type)
  mutual 
    data MT : Nat -> Type where
      Pf : novar f = true -> MT 0
      Iota1 : MT 1
      Iota2 : MT 2
      Falsum : MT 0
      Basic : o n -> MT n
      App : MT n -> (args : Vect n (m ** MT m)) -> MT (foldr (\el, accu => (fst el) + accu) 0 args)

    data MF : Type where 
      FNeg : MF -> MF
      FDia : MT n -> Vect n MF -> MF
      FProp : Nat -> MF
      FNom : Nat -> MF
      
    novar : MF -> Bool
    novar (FNeg f) = novar f
    novar (FProp _) = False
    novar (FNom _) = False
    novar (FDia _ args) = all novar args