example (x : Nat) : True :=
match h:x with

section end

structure A where
h : Nat := 1
h2 : h ≠ 0 := by