Tighten
This commit is contained in:
parent
8f20ae7a48
commit
cbbd6ffd0c
22
quoting.v
22
quoting.v
|
@ -77,24 +77,14 @@ Fixpoint pat_ind'
|
||||||
p
|
p
|
||||||
: P p.
|
: P p.
|
||||||
Proof.
|
Proof.
|
||||||
induction p; auto.
|
induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ];
|
||||||
|
try solve [ induction l; [ apply Forall_nil | ];
|
||||||
apply PRecord.
|
apply Forall_cons; [ apply pat_ind'; try assumption | ];
|
||||||
apply IHp; try assumption.
|
apply IHl ].
|
||||||
induction l; [ apply Forall_nil | ].
|
|
||||||
apply Forall_cons; [ apply pat_ind'; try assumption | ].
|
|
||||||
apply IHl; apply IHp.
|
|
||||||
|
|
||||||
apply PSeq.
|
|
||||||
induction l; [ apply Forall_nil | ].
|
|
||||||
apply Forall_cons; [ apply pat_ind'; try assumption | ].
|
|
||||||
apply IHl.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma Forall_map_map_id :
|
Lemma Forall_map_map_id : forall ps, Forall (fun p : pat => uqp (qp p) = p) ps ->
|
||||||
forall ps,
|
(map uqp (map qp ps)) = ps.
|
||||||
Forall (fun p : pat => uqp (qp p) = p) ps ->
|
|
||||||
(map uqp (map qp ps)) = ps.
|
|
||||||
Proof.
|
Proof.
|
||||||
intros; rewrite map_map; induction H; [ reflexivity | ].
|
intros; rewrite map_map; induction H; [ reflexivity | ].
|
||||||
simpl; rewrite IHForall; rewrite H; reflexivity.
|
simpl; rewrite IHForall; rewrite H; reflexivity.
|
||||||
|
|
Loading…
Reference in New Issue