proposition: Theorem si_intro : forall (X : Set) (P : X -> Prop) (x y : X) (b : bool), (b = true :>bool -> P x) -> (b = false :>bool -> P y) -> P (si X b x y).
proof: Proof. simple induction b. intros. rewrite si_eq1. apply H. trivial. intros. rewrite si_eq2. apply H0. trivial. Qed.