The Coq mailing list

[Alexander Katovsky <apk32 AT cam.ac.uk>]

Hi,

I would like to prove the lemma [OpOp] below:

Inductive Cat : Type :=
  MkCat : forall (Obj : Type)
                 (Hom : (Obj -> Obj -> Set))
                 (Id : forall x : Obj, Hom x x), Cat.

Definition Op (x : Cat) : Cat :=
  match x with
    MkCat Obj Hom Id => (MkCat Obj (fun x y => Hom y x) Id)
  end.

Lemma OpOp: forall C, C = Op(Op(C)).
  unfold Op.
  intro C.
  case C; simpl.
  intros Obj Hom Id.
  f_equal.
  intros H_Obj H_Hom H_Id.
  dependent rewrite <- H_Hom.
  (*error*)

And I get the error "Error: Cannot find a well-typed generalization of 
the goal that makes the
proof progress."  If we use [rewrite <- H_Hom] instead, we get a type 
error when Coq tries to generalize over Hom, which reveals the problem 
(the type of Id depends on Hom).

Many thanks,
Alex.