diff --git a/quoting.v b/quoting.v index 60e083b..b2976f1 100644 --- a/quoting.v +++ b/quoting.v @@ -77,24 +77,14 @@ Fixpoint pat_ind' p : P p. Proof. - induction p; auto. - - apply PRecord. - apply IHp; try assumption. - 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. + induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ]; + try solve [ induction l; [ apply Forall_nil | ]; + apply Forall_cons; [ apply pat_ind'; try assumption | ]; + apply IHl ]. Defined. -Lemma Forall_map_map_id : - forall ps, - Forall (fun p : pat => uqp (qp p) = p) ps -> - (map uqp (map qp ps)) = ps. +Lemma Forall_map_map_id : forall ps, Forall (fun p : pat => uqp (qp p) = p) ps -> + (map uqp (map qp ps)) = ps. Proof. intros; rewrite map_map; induction H; [ reflexivity | ]. simpl; rewrite IHForall; rewrite H; reflexivity.