const If_i : prop set set set const In : set set prop term iIn = In infix iIn 2000 2000 const Union : set set var x:set var g:set set set var y:set var f:set set var f2:set set hyp ~ Union y iIn y hyp If_i (Union y iIn y) (g (Union y) (f (Union y))) x = x claim If_i (Union y iIn y) (g (Union y) (f2 (Union y))) x = x -> If_i (Union y iIn y) (g (Union y) (f (Union y))) x = If_i (Union y iIn y) (g (Union y) (f2 (Union y))) x