bblum

 80           [s m = 0; % NEQS 81             0 = s m; 82           ]; 83           s m = 0 => 0 = s m; 84           [n':nat, s m = s n'; 85             m = n'; % NIS 86             m = n' => n' = m; % forall elim on x 87             n' = m; 88             s n' = s m; 89           ]; 90           n = s m;