Agda with expression; see https://blog.cppcabrera.com/posts/48-logic-proofs-with-agda-coq-idris.html

Proof.agda

module Proof where

data Or {a b} (A : Set a) (B : Set b) : Set₁ where
  Inl : A → Or A B
  Inr : B → Or A B

data And {a b} (A : Set a) (B : Set b) : Set₁ where
  AndIntro : A → B → And A B

and-dist-over-or : {a b c : Set} → And a (Or b c) → Or (And a b) (And a c)
and-dist-over-or (AndIntro a x) with x
… | Inl b = Inl (AndIntro a b)
… | Inr c = Inr (AndIntro a c)