\import{holbert-macros}
\title{Proofs!}
\taxon{Theorem}
\p{All [even](evens) numbers are natural numbers. Note that [even numbers](evens) are defined in a separate page, but changes are seamlessly synced over. }
\hol/proof{evensarenats}{
  \hol/dep{hng-0000}{config}
  \hol/dep{hng-0000}{notation}  
  \hol/dep{nats}{nat} 
  \hol/dep{evens}{evens} 
}{  
  x.
    (x Even)
    ---------------- f
    (x Nat)
  
  x. asm |- ?
}  
\hol/proof{natinversion}{
  \hol/dep{hng-0000}{config}
  \hol/dep{hng-0000}{notation}
  \hol/dep{nats}{nat} 
}{  
  x.
    ((@S x) Nat)
    ---------------- S-inv
    (x Nat)
  
  x. asm |- ?
}