| C.LetIn (nname, vv, tt) when H.is_proof c v ->
let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
HLog.warn "Optimizer: swap 1"; opt1_proof g true c x
| C.LetIn (nname, vv, tt) when H.is_proof c v ->
let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
HLog.warn "Optimizer: swap 1"; opt1_proof g true c x