Commit 6806aa48 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

maj fichier TODO

parent 8653dbfc
......@@ -3,24 +3,13 @@
- affichage court du <->
- verifier que Nam.formula_substs est bien ok
Nam:
- preuves de lemmes de substitution
- definition valid_deriv invariante par alpha
- Valid via predicat inductif + adéquation valid_deriv
- Plongement comme formules Coq + correction
Equiv:
preuves reliant Nam.valid_deriv et Mix.valid_deriv (ou Mix.Pr)
Meta
- cleanup proofs Meta
- faire les preuves de Meta directement sur Valid plutot que Pr ?
- Theoreme de complétude !!
General
- Peut-on éviter tous ces "fix IH 1" ??
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment