proposition: Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}), ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
proof: Proof. intros C decide H P H0; destruct decide. - contradiction. - apply H0. Qed.
imports: Notations Ltac Logic Specif