Update
This commit is contained in:
parent
79f9525fbd
commit
30eef734bc
@ -266,11 +266,11 @@ Proof.
|
||||
intros l hd tl. intros H I.
|
||||
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) l)).
|
||||
generalize I. generalize H. apply tm_morphism_app2.
|
||||
assert (K: l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
|
||||
symmetry. apply firstn_skipn.
|
||||
assert (K: (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l) = l).
|
||||
apply firstn_skipn.
|
||||
assert (L: tm_morphism l = (tm_morphism (firstn (Nat.div2 (length hd)) l))
|
||||
++ (tm_morphism (skipn (Nat.div2 (length hd)) l))).
|
||||
rewrite K at 1. apply tm_morphism_app.
|
||||
rewrite <- K at 1. apply tm_morphism_app.
|
||||
rewrite H in L. rewrite <- J in L.
|
||||
rewrite app_inv_head_iff in L. assumption.
|
||||
Qed.
|
||||
|
Loading…
Reference in New Issue
Block a user