---

Step * 1 1 1 of Lemma not_bfalse_btrue_const_fn_equal_union

.....assertion..... 
1. (x.tt) = (x.ff)@i
 (x.tt) = (x.ff)
BY
{ (Refine `tunionEqElimination3general` ((mk_int_arg 1).(map mk_var_arg [`w';`dn';`e';`d';`u';`v'])) THEN All Reduce)
 }

1
x.tt    

2
x.ff    

3
1. w : 
2. u :   
3. d :   
4. e : u = d
 u = d

4
1. w : 
2. u :   
3. d : x:.if x then Base else    fi 
4. dn :   
5. u = d
6. e : d = dn
7. v : u = d
 u = dn


.....assertion..... 
1.  (\mlambda{}x.tt)  =  (\mlambda{}x.ff)@i
\mvdash{}  (\mlambda{}x.tt)  =  (\mlambda{}x.ff)


By

(Refine  `tunionEqElimination3general`  ((mk\_int\_arg  1).(map  mk\_var\_arg  [`w';`dn';`e';`d';`u';`v']))\mcdot{}
  THEN  All  Reduce
  )\mcdot{}



Home Index