This commit is contained in:
Thomas Baruchel 2022-11-23 21:27:09 +01:00
parent 09e6059a4d
commit 99a4a193b6

View File

@ -1036,7 +1036,6 @@ Proof.
generalize K. generalize J. apply tm_step_stable.
rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
replace (tm_morphism (tm_step (n + m))) with (tm_step (S n + m)) in H4.
rewrite H4.
assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)).
@ -1070,10 +1069,6 @@ Proof.
rewrite H3 in H6. rewrite H5 in H6.
inversion H6. rewrite H8.
replace (tm_morphism (tm_step (n + m))) with (tm_step (S n + m)).
reflexivity.
reflexivity.
reflexivity.
Qed.