So Litex is not based on Type Theory I gather. How are proofs represented and checked?