funext v
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])
case h
D : Type
V : VarAssignment D
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ [])) v = shiftList D V (List.map (V ∘ free_) []) v