The Coq mailing list

[Cedric.Auger AT lri.fr]

Hi, i use this context:

Parameter A : Set.
Axiom A_dec : forall (a b : A), { a = b } + { a <> b }.
Parameter B : A -> Set.
Axiom B_dec : forall c (a b : B c), { a = b } + { a <> b }.
Inductive C : Set :=
C_of_B : forall a, B a -> C.

and want to prove:

Axiom C_struct : forall c (a b : B c), C_of_B c a = C_of_B c b -> a = b.

to be able to decide equality over C:

Lemma C_dec : forall (a b : C), { a = b } + { a <> b }.
Proof.
intros; destruct a; destruct b.
revert b; revert b0; destruct (A_dec a a0).
  rewrite e; clear e; intros; destruct (B_dec a0 b0 b).
    rewrite e; left; reflexivity.
    right; intro; destruct n; apply C_struct; assumption.
  intros; right; intro; inversion H; exact (n H1).
Qed.

But inversion is not enough powerfull in the way i use it, is it known to
be impossible to prove it?