import tactic norm_num def fn def t4 Prop fn fn nat prime

1
2
3
4
5
6
7
8
import tactic.norm_num
def fn(n : ) := n * 2
def t4(a b : ) : Prop :=
fn(a) = fn(b) a = b
nat.prime