Nous explorerons également la dualité entre terme de preuve et enchaînement de tactiques et les manières de les combiner, ainsi que la dualité entre un style procédural (principalement utilisé dans Coq, et correspondant à une vision dans laquelle l’utilisateur décompose un but en plusieurs sous-buts) et un style déclaratif (souvent considéré plus proche du style des démonstrations informelles).