We present constructive universal quantification and implication in miniKanren using the goal constructors (forall (v) domain goal) and (implies goal goal). Our implementation is capable of solving rudimentary logic problems while reasoning about equality, disequality, type constraints, and user-defined relations. The key idea behind handling a universal quantification (forall (v) domain goal) is to first run (exists (v) (conj domain goal)) to find a state describing some v in the domain that satisfies the goal, then use a relative complement process to generate a goal “relcomp” describing the remaining space of v not covered by that state, and then recursively search (forall (v) (conj relcomp domain) goal). The key idea behind handling an implication (implies A B) is to combine two strategies, depending on the form of A. One strategy follows the classical logic rule that “A implies B” is equivalent to “(not A) or B”, and applies when a goal A is decidable and can easily be negated. The other strategy uses syntactic pattern-matching, and applies when the antecedent goal A calls user-defined relations which match those appearing in the consequent goal B.