I don't think coq is intuitive to anyone :) It might have the steepest learning curve of any language I've learned, possibly tied with Idris, which just so happens to be another dependently typed language. The bits between Lemma and QED are kinda neat -- they're "proof tactics" written in the tactic language LTAC. It's kind of a metalanguage that directs Coq through synthesizing an actual program. Like, for example, here's a simple proposition written in LTAC: intros a b [Ha Hb]. exact Ha. Qed. and here's what Coq synthesizes for that: fun (a b : Prop) (H : a /\ b) => match H with | conj Ha _ => Ha end : forall a b : Prop, a /\ b -> a (fun is the keyword for lambdas, kinda like \ in Haskell.) In other words, that stuff is both program and proof! Lemma fst : forall a b, a /\ b -> a. fst =