22 lines
811 B
Text
22 lines
811 B
Text
|
Set: pp::colors
|
||
|
|
Set: pp::unicode
|
||
|
|
Imported 'cast'
|
||
|
|
Assumed: vec
|
||
|
|
Assumed: concat
|
||
|
|
Assumed: concat_assoc
|
||
|
|
Assumed: empty
|
||
|
|
Assumed: concat_empty
|
||
|
|
Assumed: n
|
||
|
|
Assumed: v
|
||
|
|
Assumed: w
|
||
|
|
v ; w ; empty ; (v ; empty)
|
||
|
|
===>
|
||
|
|
v ; (w ; v)
|
||
|
|
htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n))))
|
||
|
|
(to_heq (Nat::add_zeror n)))
|
||
|
|
(htrans (to_heq (concat_empty (v ; w)))
|
||
|
|
(cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w))))
|
||
|
|
(htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v)))
|
||
|
|
(to_heq (concat_assoc v w v)))
|
||
|
|
(cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v)))
|