Section if_then_else.
Variables (A:Set).
Variable dec:forall (a1 a2:A),{a1=a2}+{~a1=a2}.

Variable Res:Set.

Variables r1 r2:Res.
 
Lemma ite_l:forall (a1 a2:A), (a1=a2)-> 
(if (dec a1 a2) then r1 else r2) = r1. 
intros a1 a2 ig.
case (dec a1 a2);auto;intuition.
Qed.

Lemma ite_r:forall (a1 a2:A), (~a1=a2)->
(if (dec a1 a2) then r1 else r2)= r2. 
intros a1 a2 ig.
case (dec a1 a2);auto;intuition.
Qed.
 



End if_then_else.