QuanticPotato

Theorem rewrite_arg : 
    forall (condition : nat->Prop)(P : (forall (n:nat)(Hn : condition n),Prop))
    (arg1 arg2 : nat)(egalite : arg1 = arg2)(pArg1 : condition arg1)(pArg2 : condition arg2), 
        P arg1 pArg1 = P arg2 pArg2.

(* 1 subgoals
condition : nat -> Prop
P : forall n : nat, condition n -> Prop
arg1 : nat
arg2 : nat

QuanticPotato

match n with
    | 0 => (* sth *)
    | S p => (* I would like to have a proof [n = S p] *)
end

QuanticPotato

Section test.

Let predicate (n:nat) : Prop := n=1.
Variable a:nat.
Class class  : Prop := {
    condition : predicate a
}.

(* Another a class that requires an instance of the previous class *)
Class c2 {inst : class} := {

QuanticPotato

Section test.

(* A sample class *)
Let predicate (n:nat) : Prop := n=1.
Variable a:nat.
Class class  : Prop := {
    condition : predicate a
}.

Section nested_section.

QuanticPotato

(* La notation [=] correspond à l'infixe de Fe *)

(** Contexte **)


E : Set
Fprop : E → Prop
F := {x | Fprop x} : Set
inj := sig_injection E Fprop : {x | Fprop x} → E
Ee : Equiv E

QuanticPotato

Error:
Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.
Unable to satisfy the following constraints:
EVARS:
 ?169==[E Fprop (F:={x | Fprop x}) (inj:=sig_injection E Fprop) Ee
         Eequiv_refl Eequiv_symm Eequiv_trans x y z H
         |- ProperProxy ?167 (inj y)] (internal placeholder)
 ?168==[E Fprop (F:={x | Fprop x}) (inj:=sig_injection E Fprop) Ee
         Eequiv_refl Eequiv_symm Eequiv_trans x y z H
         (do_subrelation:=do_subrelation)

QuanticPotato

Variable I : R -> Prop.

Definition predicate_neighbourhood (P : (forall x : R, I x -> Prop)) (x0 : R) : Prop :=
    forall (x0_inf : R_inf x0),
    match x0_inf with
        | xReal H => exists (d:R), d > 0 /\ forall (x : R)(Hx : I x), Rabs (x - x0) < d -> P x Hx
        | pInf H => exists (a:R), forall (x : R)(Hx : I x), x >= a -> P x Hx
        | mInf H => exists (a:R), forall (x : R)(Hx : I x), x <= a -> P x Hx

QuanticPotato

Variable P:nat->Prop.
Variable x:nat.
Lemma test : (~ P x) -> (forall (Hx: P x), 2=2) -> False.
intros.

QuanticPotato

Variable P:nat->Prop.
Variable x:nat.
Lemma test : (~ P x) -> (forall (Hx: P x), 1) -> False.
intros.