a,b:
, e:({a..b
}
). (
i:{a..b}. e(i)) = 1 
(i:{a..b}. e(i) = 1)At: iter nat prod one iff factors one
a,b:, e:({a..b}). ( i:{a..b}. e(i)) = 1 (i:{a..b}. e(i) = 1)| By: |
a,b:, P:({a..b}Prop). (i:{a..b}. P(i)) (And i:{a..b}. P(i))
Asserted THEN Guarding ( i:<type>. <prop>) Rewrite by Hyp:-1 THEN Thin Hyp:-1
THEN Analyze |
| 1 |
b:, e:({a..b}). ( i:{a..b}. e(i)) = 1 (And i:{a..b}. e(i) = 1) | 13 steps |
About:
 |  |  |  |  |  |  |  |  |  |