Update
This commit is contained in:
parent
766adbcdd4
commit
c6142420cd
|
@ -880,7 +880,8 @@ Proof.
|
||||||
assert (J: tl (tl (tm_morphism (tm_step n))) = l2).
|
assert (J: tl (tl (tm_morphism (tm_step n))) = l2).
|
||||||
{ replace (tm_morphism (tm_step n)) with (tm_step (S n)).
|
{ replace (tm_morphism (tm_step n)) with (tm_step (S n)).
|
||||||
rewrite H. reflexivity. reflexivity. }
|
rewrite H. reflexivity. reflexivity. }
|
||||||
rewrite J.
|
rewrite J. intros. rewrite <- H1. rewrite <- H2. reflexivity.
|
||||||
|
-
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user