λn. match_nat_type False (λp. True) n

Definition not_zero : nat -> Prop := fun (n:nat) => match_nat_type (Prop) connectives.False (fun (p:nat) => connectives.True) n

definition not_zero : nat -> Prop := \lambda n : nat. (match_nat_type) (Prop) (False) (\lambda p : nat. (True) ) n

def not_zero : (nat.nat) -> Prop := fun (n : nat.nat) , ((((nat.match_nat_type) (Prop)) ((connectives.False) )) (fun (p : nat.nat) , (connectives.True) )) (n)

not_zero : [nat_sttfa.sttfa_nat -> bool] = (LAMBDA(n:nat_sttfa.sttfa_nat):nat_sttfa.match_nat_type[bool](connectives_sttfa_th.sttfa_False)((LAMBDA(p:nat_sttfa.sttfa_nat):connectives_sttfa_th.sttfa_True))(n))

Printing for OpenTheory is not working at the moment.