ex.lean

gistfile1.txt

def strict : Bool -> Type
| true => Unit
| false => Empty

def f : (n:Nat) -> strict (n > 0) -> Nat := by
  intros n
  match n with
  | .zero => simp; exact fun i => by nomatch i
  | n@(.succ _) => simp; exact fun () => n

def f2 : (n:Nat) -> (match n with | .zero => Empty | .succ _ => Unit) → Nat
  | n@(.succ _), _ => n
  | .zero, h => by simp at h; contradiction

#eval f 5 ()
#eval f2 5 ()