The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Class N : Type.
Parameter pt : N -> N.
(* type of epsilon is N->N->Prop and epsilon' is the flip of epsilon *)

Lemma pred_extens           : forall (P P' : N -> Prop), (forall n:N, P n <-> P' n) -> P = P'.
Lemma Pred_extensional   : forall (alpha beta:N->Prop), (forall a:N, alpha a <-> beta a) ->
                                                  forall phi:(N->Prop)->Prop, (phi alpha <-> phi beta).
Lemma MereoT15               : forall B C, epsilon B C /\ epsilon C B -> (forall A, epsilon A B <-> epsilon A C).
...
==============================================================
Lemma MereoT17 : forall A B C, isPartOf A B /\ singular_equality B C -> isPartOf A C.
Proof.
intros A B C H.
destruct H.
apply MereoT15 with (A:=A) in H0.
red.
unfold isPartOf in H.
apply Pred_extensional with (alpha:=epsilon' B)(beta:=epsilon' C) in H0.

===============================================================
From this point, there is a problem when using "apply Pred_extensional with (alpha:=epsilon' B)(beta:=epsilon' C) in H0." because of the "forall a:N" which is within parentheses (it generates a subgoal "forall a : N, epsilon' B a <-> epsilon' C a").
If somebody has an idea how to solve this problem?

Thanks in advance,
Richard

--

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard