theorem consfst (a b: nat): $ fst (a : b - 1) = a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
3 |
suc (a, b) - 1 = a, b |
||
4 |
conv cons |
a : b - 1 = a, b |
|
5 |
fst (a : b - 1) = fst (a, b) |
||
7 |
fst (a, b) = a |
||
8 |
eqtr* |
fst (a : b - 1) = a |