Update
This commit is contained in:
parent
14e85d0b24
commit
c067e31ecd
@ -1134,7 +1134,12 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||||||
simpl in Q. rewrite Q in H10. inversion H10.
|
simpl in Q. rewrite Q in H10. inversion H10.
|
||||||
rewrite Y''. apply Nat.le_pred_l.
|
rewrite Y''. apply Nat.le_pred_l.
|
||||||
(* now we know that b12 <> b1 *)
|
(* now we know that b12 <> b1 *)
|
||||||
|
(* proof that b12 = b0 *)
|
||||||
|
assert (b12 = b0). destruct b12; destruct b1; destruct b0.
|
||||||
|
reflexivity. contradiction n8. reflexivity. reflexivity.
|
||||||
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
||||||
|
reflexivity. contradiction n8. reflexivity. reflexivity.
|
||||||
|
rewrite H10 in H.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user