Function pi_implicit 

pub fn pi_implicit(name: &str, dom: Expr, cod: Expr) -> Expr

Build an implicit pi {name : dom} → cod.