They're almost isomorphic except for a fact that Sigma also allows Boolean literals. Another encoding is to put into leaves Either Bool ProofInput. Its advantage is that it allows to separate cases where we can have literal booleans in leaves of a Σ-expression and cases when we have Σ-expression proper.
It cuts down quite a bit of code. Another possible simplification is to use drop annotation from SigmaE and use recursion schemes machinery to annotate constructor during proof construction
They're almost isomorphic except for a fact that Sigma also allows Boolean literals. Another encoding is to put into leaves
Either Bool ProofInput. Its advantage is that it allows to separate cases where we can have literal booleans in leaves of a Σ-expression and cases when we have Σ-expression proper.It cuts down quite a bit of code. Another possible simplification is to use drop annotation from
SigmaEand use recursion schemes machinery to annotate constructor during proof construction