feat(All): Add Program.random + Axioms

[EnguerrandPrebet]

Closes #33

[EnguerrandPrebet]

I guess I did a lot more that I remembered.
I think it still misses K and I, DE and DC (though, refDE probably proves DE simpler than redoing the proof).

[eneoli]

@EnguerrandPrebet Refinement.lean imports a DLean.Math.Math file which is not part of this pr. Can you please provide these. Also make sure to add new files to the top level DLean.lean file so our checks find errors like this in future.

[eneoli]

I stumbled on these definitions:

/-- `P` is a substitute for a predicational, i.e. `k` can be uniformly substituted by any `?φ`. -/
def P := [Formula|⟨k⟩true]
def Q := [Formula|⟨l⟩true]

I assume, these are used to model predicate symbols that can depend on all variables (p(x-)).
This is justified by these equivalences:

⟨?P⟩ true
¬ [?P] false
¬ (P → false)
¬ (¬ P ∨ false)
P ∧ true
P

and P can be any predicate (-symbol). Am I right? Can you elaborate more on that?

I'm wondering if we'll get any problems since k can be an arbitrary program?