Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

 (Emilio Jesús Gallego Arias) writes:

> Definition choose_sets P :=
>   if trivIset P then set00
>   else choose cond_triv (projT1 (axC P)).
>
> Definition choose_setsP P : ~~ trivIset P ->
>   cond_triv (choose_sets P).
> Proof.
> rewrite /choose_sets; case: ifP => // /negbT tsn _.
> by apply: chooseP; case: (axC P) => //= x; rewrite tsn.
> Qed.

Well, I guess I wanted to use chooseP, but the below definition makes
a bit more sense:

Definition choose_sets P :=
  if trivIset P then set00 else projT1 (axC P).

Definition choose_setsP P : ~~ trivIset P ->
  cond_triv (choose_sets P).
Proof.
rewrite /choose_sets; case: ifP => // /negbT tsn _.
by case: (axC P) => //= x; rewrite tsn.
Qed.

E.