Option.v

Mutual Inductive Option[A:Set]: Set :=
     Some: (x:A)(Option A)
    | None: (Option A) .

Theorem SomeComp: (A:Set) (a, b:A) a=b ->(Some A a)=(Some A b).
Intros A a b H'; Rewrite H'; Auto.
Qed.
Hints Resolve SomeComp.

Inductive eqOption[A:Set; eq:A -> A ->Prop]:
   (Option A) -> (Option A) ->Prop :=
   eqOptionSome:
     (a, b:A) (eq a b) ->(eqOption A eq (Some A a) (Some A b))
  | eqOptionNone: (eqOption A eq (None A) (None A)).
Hints Resolve eqOptionSome eqOptionNone.

28/01/99, 14:29