if alpha_eq_tacterm_kerterm t1 t status goal then
let (_,_,t1) = t1 in
block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
if alpha_eq_tacterm_kerterm t1 t status goal then
let (_,_,t1) = t1 in
block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit