Added
- FunExt: axiom for functional extensionality
- PropExt: axiom for propositional extensionality and related theorems
- Prod: Cartesian product (extracted from Set)
- Option: polymorphic option type
- String: builtin string type
- Tactic: tactic type for the eval tactic
- Comp: isLe and isGe
- List: mem_tail, nths and related properties
- Bool: istrue=true
Changed
- Set: moved Cartesian product to separate Prod file, pairing constructor renamed as "‚"