equal
deleted
inserted
replaced
67 lemma "sn (Pd p) = fst p" |
67 lemma "sn (Pd p) = fst p" |
68 nitpick [expect = genuine] |
68 nitpick [expect = genuine] |
69 oops |
69 oops |
70 |
70 |
71 lemma "fs (Pd ((a, b), (c, d))) = (a, b)" |
71 lemma "fs (Pd ((a, b), (c, d))) = (a, b)" |
72 nitpick [card = 1\<midarrow>9, expect = unknown (*none*)] |
72 nitpick [card = 1\<midarrow>9, expect = none] |
73 sorry |
73 sorry |
74 |
74 |
75 lemma "fs (Pd ((a, b), (c, d))) = (c, d)" |
75 lemma "fs (Pd ((a, b), (c, d))) = (c, d)" |
76 nitpick [expect = genuine] |
76 nitpick [expect = genuine] |
77 oops |
77 oops |