| BYC_letsuchthat (id1,t1,t2,id2) ->
G.ExistsElim (loc, just, id1, t1, t2, id2)
| BYC_wehaveand (id1,t1,id2,t2) ->
G.AndElim (loc, just, t1, id1, t2, id2))
])
| BYC_letsuchthat (id1,t1,t2,id2) ->
G.ExistsElim (loc, just, id1, t1, t2, id2)
| BYC_wehaveand (id1,t1,id2,t2) ->
G.AndElim (loc, just, t1, id1, t2, id2))
])