proposition: Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.
proof: Proof. intros p q q'. induction q as [ | p q IHq ]. - apply eq_dep_eq_positive. cut (1=1). + pattern 1 at 1 2 5, q'. destruct q' as [|p ?]. * trivial. * destruct p; intros; discriminate. + trivial. - apply eq_dep_eq_positive. cut (succ p=succ p). + pattern (succ p) at 1 2 5, q'. destruct q' as [|? q']. * intro. destruct p; discriminate. * intro H. apply succ_inj in H. generalize q'. rewrite H. intro q'0. rewrite (IHq q'0). trivial. + trivial. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef