fact: Definition delta : exp -> exp := fun e=> match e with | B band ffalse e' => ffalse | B band nil e' => ffalse | B band _ e' => e' | B bor ffalse e' => e' | B bor nil e' => e' | B bor v e' => v | U not ffalse => ttrue | U not nil => ttrue | U not _ => ffalse | _ => e end.