(NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
(NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)