fact: Definition LIP_rcons := fix f l1 := match l1 with | lnil => fun ip => ip | lcons ip1 l1 => fun ip => lcons ip1 (f l1 ip) end.
imports: Coq.Strings.String Mtac2(List Base) Mtac2.tactics(TacticsBase Tactics ImportedTactics)