Program Lemma if_sumbool_morphism : forall [ Equivalence A equ ] {P : Prop} (t : { P } + { ~ P })
  {P' : Prop}  (t' : { P' } + { ~ P' }), P === P' -> 
  forall (x x' y y' : A), x === x' -> y === y' -> (if t then x else y) === (if t' then x' else y').
Proof with triv.
  intros.
  destruct t ; destruct t' ; simpl ; auto.
  pose (proj1 H0 p) ; contradiction.
  pose (proj2 H0 p) ; contradiction.
Qed.