proposition: Theorem PExpr_eq_semi_ok e e' : PExpr_eq e e' = true -> (e === e')%poly.
proof: Proof. revert e'; induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe ?]; intro e'; destruct e'; simpl; try discriminate. - intros H l. now apply (morph_eq CRmorph). - case Pos.eqb_spec; intros; now subst. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H. now rewrite IHe. - intros H. destruct (if_true _ _ H) as [H0 H1]. apply N.eqb_eq in H0. now rewrite IHe, H0. Qed.
imports: ZArith_base