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